Theorem uniss 4490

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 3630	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 588	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1886	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4471	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4471	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 285	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3642	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 383  ∃wex 1744   ∈ wcel 2030   ⊆ wss 3607  ∪ cuni 4468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-uni 4469

This theorem is referenced by:  unissi  4493  unissd  4494  intssuni2  4534  uniintsn  4546  relfld  5699  dffv2  6310  trcl  8642  cflm  9110  coflim  9121  cfslbn  9127  fin23lem41  9212  fin1a2lem12  9271  tskuni  9643  prdsval  16162  prdsbas  16164  prdsplusg  16165  prdsmulr  16166  prdsvsca  16167  prdshom  16174  mrcssv  16321  catcfuccl  16806  catcxpccl  16894  mrelatlub  17233  mreclatBAD  17234  dprdres  18473  dmdprdsplit2lem  18490  tgcl  20821  distop  20847  fctop  20856  cctop  20858  neiptoptop  20983  cmpcld  21253  uncmp  21254  cmpfi  21259  comppfsc  21383  kgentopon  21389  txcmplem2  21493  filconn  21734  alexsubALTlem3  21900  alexsubALT  21902  ptcmplem3  21905  dyadmbllem  23413  shsupcl  28325  hsupss  28328  shatomistici  29348  pwuniss  29496  carsggect  30508  carsgclctun  30511  cvmliftlem15  31406  frrlem5c  31911  filnetlem3  32500  icoreunrn  33337  heiborlem1  33740  lssats  34617  lpssat  34618  lssatle  34620  lssat  34621  dicval  36782  pwsal  40853  prsal  40856  intsaluni  40865