Theorem uniss 4394

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 3562	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 587	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1833	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4375	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4375	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 284	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3574	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 383  ∃wex 1695   ∈ wcel 1977   ⊆ wss 3540  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-uni 4373

This theorem is referenced by:  unissi  4397  unissd  4398  intssuni2  4437  uniintsn  4449  relfld  5578  dffv2  6181  trcl  8487  cflm  8955  coflim  8966  cfslbn  8972  fin23lem41  9057  fin1a2lem12  9116  tskuni  9484  prdsval  15938  prdsbas  15940  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  prdshom  15950  mrcssv  16097  catcfuccl  16582  catcxpccl  16670  mrelatlub  17009  mreclatBAD  17010  dprdres  18250  dmdprdsplit2lem  18267  tgcl  20584  distop  20610  fctop  20618  cctop  20620  neiptoptop  20745  cmpcld  21015  uncmp  21016  cmpfi  21021  comppfsc  21145  kgentopon  21151  txcmplem2  21255  filcon  21497  alexsubALTlem3  21663  alexsubALT  21665  ptcmplem3  21668  dyadmbllem  23173  shsupcl  27581  hsupss  27584  shatomistici  28604  pwuniss  28753  carsggect  29707  carsgclctun  29710  cvmliftlem15  30534  frrlem5c  31030  filnetlem3  31545  icoreunrn  32383  heiborlem1  32780  lssats  33317  lpssat  33318  lssatle  33320  lssat  33321  dicval  35483  pwsal  39211  prsal  39214  intsaluni  39223