Theorem uniss 4869

Description: Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
uniss	⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Proof of Theorem uniss

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3931	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 612	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1917	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4864	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4864	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3943	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109   ⊆ wss 3905  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-uni 4862

This theorem is referenced by:  unissi  4870  unissd  4871  intssuni2  4926  uniintsn  4938  relfld  6227  dffv2  6922  trcl  9643  cflm  10163  coflim  10174  cfslbn  10180  fin23lem41  10265  fin1a2lem12  10324  tskuni  10696  prdsvallem  17376  prdsval  17377  prdsbas  17379  prdsplusg  17380  prdsmulr  17381  prdsvsca  17382  prdshom  17389  mrcssv  17538  catcfuccl  18043  catcxpccl  18131  mrelatlub  18486  mreclatBAD  18487  dprdres  19927  dmdprdsplit2lem  19944  tgcl  22872  distop  22898  fctop  22907  cctop  22909  neiptoptop  23034  cmpcld  23305  uncmp  23306  cmpfi  23311  comppfsc  23435  kgentopon  23441  txcmplem2  23545  filconn  23786  alexsubALTlem3  23952  alexsubALT  23954  ptcmplem3  23957  dyadmbllem  25516  shsupcl  31300  hsupss  31303  shatomistici  32323  carsggect  34285  cvmliftlem15  35270  filnetlem3  36353  icoreunrn  37332  ctbssinf  37379  pibt2  37390  heiborlem1  37790  lssats  38990  lpssat  38991  lssatle  38993  lssat  38994  dicval  41155  onsupneqmaxlim0  43197  onsupnmax  43201  onsssupeqcond  43253  mreuniss  48885