Theorem uniss 4872

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 3930	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 621	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1936	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4867	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4867	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 298	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3942	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1798   ∈ wcel 2141   ⊆ wss 3904  ∪ cuni 4864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-uni 4865

This theorem is referenced by:  unissi  4873  unissd  4874  intssuni2  4930  uniintsn  4942  relfld  6258  dffv2  6958  trcl  9680  cflm  10203  coflim  10215  cfslbn  10221  fin23lem41  10306  fin1a2lem12  10365  tskuni  10738  prdsvallem  17466  prdsval  17467  prdsbas  17469  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  prdshom  17479  mrcssv  17629  catcfuccl  18134  catcxpccl  18222  mrelatlub  18577  mreclatBAD  18578  dprdres  20053  dmdprdsplit2lem  20070  tgcl  23009  distop  23035  fctop  23044  cctop  23046  neiptoptop  23171  cmpcld  23442  uncmp  23443  cmpfi  23448  comppfsc  23572  kgentopon  23578  txcmplem2  23682  filconn  23923  alexsubALTlem3  24089  alexsubALT  24091  ptcmplem3  24094  dyadmbllem  25641  shsupcl  31487  hsupss  31490  shatomistici  32510  carsggect  34576  cvmliftlem15  35612  filnetlem3  36704  ttcmin  36820  dfttc2g  36830  icoreunrn  37817  ctbssinf  37864  pibt2  37875  heiborlem1  38274  lssats  39600  lpssat  39601  lssatle  39603  lssat  39604  dicval  41764  onsupneqmaxlim0  43765  onsupnmax  43769  onsssupeqcond  43821  mreuniss  49485