Theorem uniss 4874

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1811   ∈ wcel 2144   ⊆ wss 3895  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867

This theorem is used by:  unissi  4875  unissd  4876  intssuni2  4932  uniintsn  4944  relfld  6277  dffv2  6980  trcl  9732  cflm  10330  coflim  10342  cfslbn  10348  fin23lem41  10433  fin1a2lem12  10492  tskuni  10871  prdsvallem  17630  prdsval  17631  prdsbas  17633  prdsplusg  17634  prdsmulr  17635  prdsvsca  17636  prdshom  17643  mrcssv  17793  catcfuccl  18298  catcxpccl  18386  mrelatlub  18741  mreclatBAD  18742  dprdres  20249  dmdprdsplit2lem  20266  tgcl  23292  distop  23318  fctop  23327  cctop  23329  neiptoptop  23454  cmpcld  23725  uncmp  23726  cmpfi  23731  comppfsc  23856  kgentopon  23862  txcmplem2  23966  filconn  24207  alexsubALTlem3  24373  alexsubALT  24375  ptcmplem3  24378  dyadmbllem  25925  shsupcl  31945  hsupss  31948  shatomistici  32968  carsggect  34996  cvmliftlem15  36149  filnetlem3  37260  ttcmin  37376  dfttc2g  37386  icoreunrn  38375  ctbssinf  38422  pibt2  38433  heiborlem1  38838  lssats  40162  lpssat  40163  lssatle  40165  lssat  40166  dicval  42326  onsupneqmaxlim0  44319  onsupnmax  44323  onsssupeqcond  44375  mreuniss  50107