Theorem uniss 4809

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

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

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 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-uni 4802

This theorem is referenced by:  unissi  4810  unissd  4811  intssuni2  4866  uniintsn  4880  relfld  6109  dffv2  6752  trcl  9216  cflm  9723  coflim  9734  cfslbn  9740  fin23lem41  9825  fin1a2lem12  9884  tskuni  10256  prdsval  16800  prdsbas  16802  prdsplusg  16803  prdsmulr  16804  prdsvsca  16805  prdshom  16812  mrcssv  16957  catcfuccl  17449  catcxpccl  17537  mrelatlub  17876  mreclatBAD  17877  dprdres  19232  dmdprdsplit2lem  19249  tgcl  21683  distop  21709  fctop  21718  cctop  21720  neiptoptop  21845  cmpcld  22116  uncmp  22117  cmpfi  22122  comppfsc  22246  kgentopon  22252  txcmplem2  22356  filconn  22597  alexsubALTlem3  22763  alexsubALT  22765  ptcmplem3  22768  dyadmbllem  24313  shsupcl  29234  hsupss  29237  shatomistici  30257  carsggect  31817  cvmliftlem15  32789  filnetlem3  34153  icoreunrn  35091  ctbssinf  35138  pibt2  35149  heiborlem1  35564  lssats  36623  lpssat  36624  lssatle  36626  lssat  36627  dicval  38787