Theorem uniss 4853

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 3916	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 618	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1924	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4848	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4848	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 297	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3928	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1786   ∈ wcel 2119   ⊆ wss 3890  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-uni 4846

This theorem is referenced by:  unissi  4854  unissd  4855  intssuni2  4910  uniintsn  4922  relfld  6233  dffv2  6929  trcl  9647  cflm  10170  coflim  10181  cfslbn  10187  fin23lem41  10272  fin1a2lem12  10331  tskuni  10704  prdsvallem  17415  prdsval  17416  prdsbas  17418  prdsplusg  17419  prdsmulr  17420  prdsvsca  17421  prdshom  17428  mrcssv  17578  catcfuccl  18083  catcxpccl  18171  mrelatlub  18526  mreclatBAD  18527  dprdres  20003  dmdprdsplit2lem  20020  tgcl  22959  distop  22985  fctop  22994  cctop  22996  neiptoptop  23121  cmpcld  23392  uncmp  23393  cmpfi  23398  comppfsc  23522  kgentopon  23528  txcmplem2  23632  filconn  23873  alexsubALTlem3  24039  alexsubALT  24041  ptcmplem3  24044  dyadmbllem  25591  shsupcl  31434  hsupss  31437  shatomistici  32457  carsggect  34509  cvmliftlem15  35533  filnetlem3  36615  ttcmin  36731  dfttc2g  36741  icoreunrn  37728  ctbssinf  37775  pibt2  37786  heiborlem1  38185  lssats  39511  lpssat  39512  lssatle  39514  lssat  39515  dicval  41675  onsupneqmaxlim0  43676  onsupnmax  43680  onsssupeqcond  43732  mreuniss  49397