Theorem uniss 4852

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

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1776   ∈ wcel 2110   ⊆ wss 3935  ∪ cuni 4831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942  df-ss 3951  df-uni 4832

This theorem is referenced by:  unissi  4854  unissd  4855  intssuni2  4893  uniintsn  4905  relfld  6120  dffv2  6750  trcl  9164  cflm  9666  coflim  9677  cfslbn  9683  fin23lem41  9768  fin1a2lem12  9827  tskuni  10199  prdsval  16722  prdsbas  16724  prdsplusg  16725  prdsmulr  16726  prdsvsca  16727  prdshom  16734  mrcssv  16879  catcfuccl  17363  catcxpccl  17451  mrelatlub  17790  mreclatBAD  17791  dprdres  19144  dmdprdsplit2lem  19161  tgcl  21571  distop  21597  fctop  21606  cctop  21608  neiptoptop  21733  cmpcld  22004  uncmp  22005  cmpfi  22010  comppfsc  22134  kgentopon  22140  txcmplem2  22244  filconn  22485  alexsubALTlem3  22651  alexsubALT  22653  ptcmplem3  22656  dyadmbllem  24194  shsupcl  29109  hsupss  29112  shatomistici  30132  carsggect  31571  carsgclctun  31574  cvmliftlem15  32540  filnetlem3  33723  icoreunrn  34634  ctbssinf  34681  pibt2  34692  heiborlem1  35083  lssats  36142  lpssat  36143  lssatle  36145  lssat  36146  dicval  38306  pwsal  42594  intsaluni  42606