Theorem uniss 4875

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 3925	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 624	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1950	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4870	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4870	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3937	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2145   ⊆ wss 3899  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868

This theorem is used by:  unissi  4876  unissd  4877  intssuni2  4933  uniintsn  4945  relfld  6270  dffv2  6972  trcl  9713  cflm  10308  coflim  10320  cfslbn  10326  fin23lem41  10411  fin1a2lem12  10470  tskuni  10849  prdsvallem  17605  prdsval  17606  prdsbas  17608  prdsplusg  17609  prdsmulr  17610  prdsvsca  17611  prdshom  17618  mrcssv  17768  catcfuccl  18273  catcxpccl  18361  mrelatlub  18716  mreclatBAD  18717  dprdres  20224  dmdprdsplit2lem  20241  tgcl  23267  distop  23293  fctop  23302  cctop  23304  neiptoptop  23429  cmpcld  23700  uncmp  23701  cmpfi  23706  comppfsc  23831  kgentopon  23837  txcmplem2  23941  filconn  24182  alexsubALTlem3  24348  alexsubALT  24350  ptcmplem3  24353  dyadmbllem  25900  shsupcl  31922  hsupss  31925  shatomistici  32945  carsggect  34933  cvmliftlem15  36032  filnetlem3  37138  ttcmin  37254  dfttc2g  37264  icoreunrn  38250  ctbssinf  38297  pibt2  38308  heiborlem1  38713  lssats  40037  lpssat  40038  lssatle  40040  lssat  40041  dicval  42201  onsupneqmaxlim0  44184  onsupnmax  44188  onsssupeqcond  44240  mreuniss  49952