Theorem uniss 4867

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2111   ⊆ wss 3902  ∪ cuni 4859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-uni 4860

This theorem is referenced by:  unissi  4868  unissd  4869  intssuni2  4923  uniintsn  4935  relfld  6222  dffv2  6917  trcl  9618  cflm  10138  coflim  10149  cfslbn  10155  fin23lem41  10240  fin1a2lem12  10299  tskuni  10671  prdsvallem  17355  prdsval  17356  prdsbas  17358  prdsplusg  17359  prdsmulr  17360  prdsvsca  17361  prdshom  17368  mrcssv  17517  catcfuccl  18022  catcxpccl  18110  mrelatlub  18465  mreclatBAD  18466  dprdres  19940  dmdprdsplit2lem  19957  tgcl  22882  distop  22908  fctop  22917  cctop  22919  neiptoptop  23044  cmpcld  23315  uncmp  23316  cmpfi  23321  comppfsc  23445  kgentopon  23451  txcmplem2  23555  filconn  23796  alexsubALTlem3  23962  alexsubALT  23964  ptcmplem3  23967  dyadmbllem  25525  shsupcl  31313  hsupss  31316  shatomistici  32336  carsggect  34326  cvmliftlem15  35330  filnetlem3  36413  icoreunrn  37392  ctbssinf  37439  pibt2  37450  heiborlem1  37850  lssats  39050  lpssat  39051  lssatle  39053  lssat  39054  dicval  41214  onsupneqmaxlim0  43256  onsupnmax  43260  onsssupeqcond  43312  mreuniss  48930