Theorem uniss 4847

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1782   ∈ wcel 2106   ⊆ wss 3887  ∪ cuni 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840

This theorem is referenced by:  unissi  4848  unissd  4849  intssuni2  4904  uniintsn  4918  relfld  6178  dffv2  6863  trcl  9486  cflm  10006  coflim  10017  cfslbn  10023  fin23lem41  10108  fin1a2lem12  10167  tskuni  10539  prdsvallem  17165  prdsval  17166  prdsbas  17168  prdsplusg  17169  prdsmulr  17170  prdsvsca  17171  prdshom  17178  mrcssv  17323  catcfuccl  17834  catcfucclOLD  17835  catcxpccl  17924  catcxpcclOLD  17925  mrelatlub  18280  mreclatBAD  18281  dprdres  19631  dmdprdsplit2lem  19648  tgcl  22119  distop  22145  fctop  22154  cctop  22156  neiptoptop  22282  cmpcld  22553  uncmp  22554  cmpfi  22559  comppfsc  22683  kgentopon  22689  txcmplem2  22793  filconn  23034  alexsubALTlem3  23200  alexsubALT  23202  ptcmplem3  23205  dyadmbllem  24763  shsupcl  29700  hsupss  29703  shatomistici  30723  carsggect  32285  cvmliftlem15  33260  filnetlem3  34569  icoreunrn  35530  ctbssinf  35577  pibt2  35588  heiborlem1  35969  lssats  37026  lpssat  37027  lssatle  37029  lssat  37030  dicval  39190  mreuniss  46193