Theorem uniss 4649

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 3790	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 606	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 2013	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4629	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4629	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 288	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3802	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 385  ∃wex 1875   ∈ wcel 2157   ⊆ wss 3767  ∪ cuni 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-v 3385  df-in 3774  df-ss 3781  df-uni 4627

This theorem is referenced by:  unissi  4651  unissd  4652  intssuni2  4690  uniintsn  4702  relfld  5878  dffv2  6494  trcl  8852  cflm  9358  coflim  9369  cfslbn  9375  fin23lem41  9460  fin1a2lem12  9519  tskuni  9891  prdsval  16427  prdsbas  16429  prdsplusg  16430  prdsmulr  16431  prdsvsca  16432  prdshom  16439  mrcssv  16586  catcfuccl  17070  catcxpccl  17159  mrelatlub  17498  mreclatBAD  17499  dprdres  18740  dmdprdsplit2lem  18757  tgcl  21099  distop  21125  fctop  21134  cctop  21136  neiptoptop  21261  cmpcld  21531  uncmp  21532  cmpfi  21537  comppfsc  21661  kgentopon  21667  txcmplem2  21771  filconn  22012  alexsubALTlem3  22178  alexsubALT  22180  ptcmplem3  22183  dyadmbllem  23704  shsupcl  28714  hsupss  28717  shatomistici  29737  pwuniss  29880  carsggect  30888  carsgclctun  30891  cvmliftlem15  31789  frrlem5c  32291  filnetlem3  32879  icoreunrn  33697  heiborlem1  34089  lssats  35025  lpssat  35026  lssatle  35028  lssat  35029  dicval  37189  pwsal  41266  prsal  41269  intsaluni  41278