Theorem uniss 4879

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

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

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 3449  df-ss 3931  df-uni 4872

This theorem is referenced by:  unissi  4880  unissd  4881  intssuni2  4937  uniintsn  4949  relfld  6248  dffv2  6956  trcl  9681  cflm  10203  coflim  10214  cfslbn  10220  fin23lem41  10305  fin1a2lem12  10364  tskuni  10736  prdsvallem  17417  prdsval  17418  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  mrcssv  17575  catcfuccl  18080  catcxpccl  18168  mrelatlub  18521  mreclatBAD  18522  dprdres  19960  dmdprdsplit2lem  19977  tgcl  22856  distop  22882  fctop  22891  cctop  22893  neiptoptop  23018  cmpcld  23289  uncmp  23290  cmpfi  23295  comppfsc  23419  kgentopon  23425  txcmplem2  23529  filconn  23770  alexsubALTlem3  23936  alexsubALT  23938  ptcmplem3  23941  dyadmbllem  25500  shsupcl  31267  hsupss  31270  shatomistici  32290  carsggect  34309  cvmliftlem15  35285  filnetlem3  36368  icoreunrn  37347  ctbssinf  37394  pibt2  37405  heiborlem1  37805  lssats  39005  lpssat  39006  lssatle  39008  lssat  39009  dicval  41170  onsupneqmaxlim0  43213  onsupnmax  43217  onsssupeqcond  43269  mreuniss  48888