Theorem uniss 4878

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 3907	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 624	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1952	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4873	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4873	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3919	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2147   ⊆ wss 3900  ∪ cuni 4870

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871

This theorem is used by:  unissi  4879  unissd  4880  intssuni2  4936  uniintsn  4948  relfld  6296  dffv2  7006  trcl  9759  cflm  10357  coflim  10369  cfslbn  10375  fin23lem41  10460  fin1a2lem12  10519  tskuni  10898  prdsvallem  17657  prdsval  17658  prdsbas  17660  prdsplusg  17661  prdsmulr  17662  prdsvsca  17663  prdshom  17670  mrcssv  17820  catcfuccl  18325  catcxpccl  18413  mrelatlub  18768  mreclatBAD  18769  dprdres  20277  dmdprdsplit2lem  20294  tgcl  23320  distop  23346  fctop  23355  cctop  23357  neiptoptop  23482  cmpcld  23753  uncmp  23754  cmpfi  23759  comppfsc  23884  kgentopon  23890  txcmplem2  23994  filconn  24235  alexsubALTlem3  24401  alexsubALT  24403  ptcmplem3  24406  dyadmbllem  25953  shsupcl  31973  hsupss  31976  shatomistici  32996  carsggect  35033  cvmliftlem15  36243  filnetlem3  37359  ttcmin  37475  dfttc2g  37485  icoreunrn  38487  ctbssinf  38534  pibt2  38545  heiborlem1  38948  lssats  40272  lpssat  40273  lssatle  40275  lssat  40276  dicval  42436  onsupneqmaxlim0  44429  onsupnmax  44433  onsssupeqcond  44485  mreuniss  50229