Theorem uniss 4866

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 3924	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 612	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1918	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4861	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4861	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3936	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2113   ⊆ wss 3898  ∪ cuni 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-uni 4859

This theorem is referenced by:  unissi  4867  unissd  4868  intssuni2  4923  uniintsn  4935  relfld  6227  dffv2  6923  trcl  9625  cflm  10148  coflim  10159  cfslbn  10165  fin23lem41  10250  fin1a2lem12  10309  tskuni  10681  prdsvallem  17360  prdsval  17361  prdsbas  17363  prdsplusg  17364  prdsmulr  17365  prdsvsca  17366  prdshom  17373  mrcssv  17522  catcfuccl  18027  catcxpccl  18115  mrelatlub  18470  mreclatBAD  18471  dprdres  19944  dmdprdsplit2lem  19961  tgcl  22885  distop  22911  fctop  22920  cctop  22922  neiptoptop  23047  cmpcld  23318  uncmp  23319  cmpfi  23324  comppfsc  23448  kgentopon  23454  txcmplem2  23558  filconn  23799  alexsubALTlem3  23965  alexsubALT  23967  ptcmplem3  23970  dyadmbllem  25528  shsupcl  31320  hsupss  31323  shatomistici  32343  carsggect  34352  cvmliftlem15  35363  filnetlem3  36445  icoreunrn  37424  ctbssinf  37471  pibt2  37482  heiborlem1  37871  lssats  39131  lpssat  39132  lssatle  39134  lssat  39135  dicval  41295  onsupneqmaxlim0  43341  onsupnmax  43345  onsssupeqcond  43397  mreuniss  49024