Theorem uniss 4881

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 3939	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 623	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1944	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4876	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4876	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3951	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1806   ∈ wcel 2149   ⊆ wss 3913  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-uni 4874

This theorem is referenced by:  unissi  4882  unissd  4883  intssuni2  4939  uniintsn  4951  relfld  6274  dffv2  6974  trcl  9693  cflm  10229  coflim  10241  cfslbn  10247  fin23lem41  10332  fin1a2lem12  10391  tskuni  10764  prdsvallem  17503  prdsval  17504  prdsbas  17506  prdsplusg  17507  prdsmulr  17508  prdsvsca  17509  prdshom  17516  mrcssv  17666  catcfuccl  18171  catcxpccl  18259  mrelatlub  18614  mreclatBAD  18615  dprdres  20096  dmdprdsplit2lem  20113  tgcl  23091  distop  23117  fctop  23126  cctop  23128  neiptoptop  23253  cmpcld  23524  uncmp  23525  cmpfi  23530  comppfsc  23654  kgentopon  23660  txcmplem2  23764  filconn  24005  alexsubALTlem3  24171  alexsubALT  24173  ptcmplem3  24176  dyadmbllem  25723  shsupcl  31627  hsupss  31630  shatomistici  32650  carsggect  34649  cvmliftlem15  35685  filnetlem3  36776  ttcmin  36892  dfttc2g  36902  icoreunrn  37888  ctbssinf  37935  pibt2  37946  heiborlem1  38345  lssats  39671  lpssat  39672  lssatle  39674  lssat  39675  dicval  41835  onsupneqmaxlim0  43838  onsupnmax  43842  onsssupeqcond  43894  mreuniss  49558