Theorem uniss 4808

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 3908	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 614	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1918	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4803	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4803	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3921	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1781   ∈ wcel 2111   ⊆ wss 3881  ∪ cuni 4800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801

This theorem is referenced by:  unissi  4809  unissd  4810  intssuni2  4863  uniintsn  4875  relfld  6094  dffv2  6733  trcl  9154  cflm  9661  coflim  9672  cfslbn  9678  fin23lem41  9763  fin1a2lem12  9822  tskuni  10194  prdsval  16720  prdsbas  16722  prdsplusg  16723  prdsmulr  16724  prdsvsca  16725  prdshom  16732  mrcssv  16877  catcfuccl  17361  catcxpccl  17449  mrelatlub  17788  mreclatBAD  17789  dprdres  19143  dmdprdsplit2lem  19160  tgcl  21574  distop  21600  fctop  21609  cctop  21611  neiptoptop  21736  cmpcld  22007  uncmp  22008  cmpfi  22013  comppfsc  22137  kgentopon  22143  txcmplem2  22247  filconn  22488  alexsubALTlem3  22654  alexsubALT  22656  ptcmplem3  22659  dyadmbllem  24203  shsupcl  29121  hsupss  29124  shatomistici  30144  carsggect  31686  cvmliftlem15  32658  filnetlem3  33841  icoreunrn  34776  ctbssinf  34823  pibt2  34834  heiborlem1  35249  lssats  36308  lpssat  36309  lssatle  36311  lssat  36312  dicval  38472