Theorem uniss 4866

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109   ⊆ wss 3903  ∪ cuni 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-uni 4859

This theorem is referenced by:  unissi  4867  unissd  4868  intssuni2  4923  uniintsn  4935  relfld  6223  dffv2  6918  trcl  9624  cflm  10144  coflim  10155  cfslbn  10161  fin23lem41  10246  fin1a2lem12  10305  tskuni  10677  prdsvallem  17358  prdsval  17359  prdsbas  17361  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  prdshom  17371  mrcssv  17520  catcfuccl  18025  catcxpccl  18113  mrelatlub  18468  mreclatBAD  18469  dprdres  19909  dmdprdsplit2lem  19926  tgcl  22854  distop  22880  fctop  22889  cctop  22891  neiptoptop  23016  cmpcld  23287  uncmp  23288  cmpfi  23293  comppfsc  23417  kgentopon  23423  txcmplem2  23527  filconn  23768  alexsubALTlem3  23934  alexsubALT  23936  ptcmplem3  23939  dyadmbllem  25498  shsupcl  31286  hsupss  31289  shatomistici  32309  carsggect  34302  cvmliftlem15  35291  filnetlem3  36374  icoreunrn  37353  ctbssinf  37400  pibt2  37411  heiborlem1  37811  lssats  39011  lpssat  39012  lssatle  39014  lssat  39015  dicval  41175  onsupneqmaxlim0  43217  onsupnmax  43221  onsssupeqcond  43273  mreuniss  48904