Theorem uniss 4844

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 3910	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 611	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1921	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4839	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4839	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 295	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3923	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1783   ∈ wcel 2108   ⊆ wss 3883  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837

This theorem is referenced by:  unissi  4845  unissd  4846  intssuni2  4901  uniintsn  4915  relfld  6167  dffv2  6845  trcl  9417  cflm  9937  coflim  9948  cfslbn  9954  fin23lem41  10039  fin1a2lem12  10098  tskuni  10470  prdsvallem  17082  prdsval  17083  prdsbas  17085  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  prdshom  17095  mrcssv  17240  catcfuccl  17750  catcfucclOLD  17751  catcxpccl  17840  catcxpcclOLD  17841  mrelatlub  18195  mreclatBAD  18196  dprdres  19546  dmdprdsplit2lem  19563  tgcl  22027  distop  22053  fctop  22062  cctop  22064  neiptoptop  22190  cmpcld  22461  uncmp  22462  cmpfi  22467  comppfsc  22591  kgentopon  22597  txcmplem2  22701  filconn  22942  alexsubALTlem3  23108  alexsubALT  23110  ptcmplem3  23113  dyadmbllem  24668  shsupcl  29601  hsupss  29604  shatomistici  30624  carsggect  32185  cvmliftlem15  33160  filnetlem3  34496  icoreunrn  35457  ctbssinf  35504  pibt2  35515  heiborlem1  35896  lssats  36953  lpssat  36954  lssatle  36956  lssat  36957  dicval  39117  mreuniss  46081