Theorem uniss 4848

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 3963	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 613	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1918	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4843	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4843	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 298	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3975	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1780   ∈ wcel 2114   ⊆ wss 3938  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841

This theorem is referenced by:  unissi  4849  unissd  4850  intssuni2  4903  uniintsn  4915  relfld  6128  dffv2  6758  trcl  9172  cflm  9674  coflim  9685  cfslbn  9691  fin23lem41  9776  fin1a2lem12  9835  tskuni  10207  prdsval  16730  prdsbas  16732  prdsplusg  16733  prdsmulr  16734  prdsvsca  16735  prdshom  16742  mrcssv  16887  catcfuccl  17371  catcxpccl  17459  mrelatlub  17798  mreclatBAD  17799  dprdres  19152  dmdprdsplit2lem  19169  tgcl  21579  distop  21605  fctop  21614  cctop  21616  neiptoptop  21741  cmpcld  22012  uncmp  22013  cmpfi  22018  comppfsc  22142  kgentopon  22148  txcmplem2  22252  filconn  22493  alexsubALTlem3  22659  alexsubALT  22661  ptcmplem3  22664  dyadmbllem  24202  shsupcl  29117  hsupss  29120  shatomistici  30140  carsggect  31578  cvmliftlem15  32547  filnetlem3  33730  icoreunrn  34642  ctbssinf  34689  pibt2  34700  heiborlem1  35091  lssats  36150  lpssat  36151  lssatle  36153  lssat  36154  dicval  38314