Theorem uniss 4882

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875

This theorem is referenced by:  unissi  4883  unissd  4884  intssuni2  4940  uniintsn  4952  relfld  6251  dffv2  6959  trcl  9688  cflm  10210  coflim  10221  cfslbn  10227  fin23lem41  10312  fin1a2lem12  10371  tskuni  10743  prdsvallem  17424  prdsval  17425  prdsbas  17427  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  prdshom  17437  mrcssv  17582  catcfuccl  18087  catcxpccl  18175  mrelatlub  18528  mreclatBAD  18529  dprdres  19967  dmdprdsplit2lem  19984  tgcl  22863  distop  22889  fctop  22898  cctop  22900  neiptoptop  23025  cmpcld  23296  uncmp  23297  cmpfi  23302  comppfsc  23426  kgentopon  23432  txcmplem2  23536  filconn  23777  alexsubALTlem3  23943  alexsubALT  23945  ptcmplem3  23948  dyadmbllem  25507  shsupcl  31274  hsupss  31277  shatomistici  32297  carsggect  34316  cvmliftlem15  35292  filnetlem3  36375  icoreunrn  37354  ctbssinf  37401  pibt2  37412  heiborlem1  37812  lssats  39012  lpssat  39013  lssatle  39015  lssat  39016  dicval  41177  onsupneqmaxlim0  43220  onsupnmax  43224  onsssupeqcond  43276  mreuniss  48892