Theorem uniss 4873

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114   ⊆ wss 3903  ∪ cuni 4865

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866

This theorem is referenced by:  unissi  4874  unissd  4875  intssuni2  4930  uniintsn  4942  relfld  6241  dffv2  6937  trcl  9649  cflm  10172  coflim  10183  cfslbn  10189  fin23lem41  10274  fin1a2lem12  10333  tskuni  10706  prdsvallem  17386  prdsval  17387  prdsbas  17389  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  prdshom  17399  mrcssv  17549  catcfuccl  18054  catcxpccl  18142  mrelatlub  18497  mreclatBAD  18498  dprdres  19971  dmdprdsplit2lem  19988  tgcl  22925  distop  22951  fctop  22960  cctop  22962  neiptoptop  23087  cmpcld  23358  uncmp  23359  cmpfi  23364  comppfsc  23488  kgentopon  23494  txcmplem2  23598  filconn  23839  alexsubALTlem3  24005  alexsubALT  24007  ptcmplem3  24010  dyadmbllem  25568  shsupcl  31425  hsupss  31428  shatomistici  32448  carsggect  34495  cvmliftlem15  35511  filnetlem3  36593  icoreunrn  37608  ctbssinf  37655  pibt2  37666  heiborlem1  38056  lssats  39382  lpssat  39383  lssatle  39385  lssat  39386  dicval  41546  onsupneqmaxlim0  43575  onsupnmax  43579  onsssupeqcond  43631  mreuniss  49253