Theorem uniss 4881

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 3932	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 623	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1947	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4876	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4876	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3944	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1809   ∈ wcel 2143   ⊆ wss 3906  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-uni 4874

This theorem is referenced by:  unissi  4882  unissd  4883  intssuni2  4939  uniintsn  4951  relfld  6278  dffv2  6978  trcl  9698  cflm  10234  coflim  10246  cfslbn  10252  fin23lem41  10337  fin1a2lem12  10396  tskuni  10769  prdsvallem  17508  prdsval  17509  prdsbas  17511  prdsplusg  17512  prdsmulr  17513  prdsvsca  17514  prdshom  17521  mrcssv  17671  catcfuccl  18176  catcxpccl  18264  mrelatlub  18619  mreclatBAD  18620  dprdres  20101  dmdprdsplit2lem  20118  tgcl  23107  distop  23133  fctop  23142  cctop  23144  neiptoptop  23269  cmpcld  23540  uncmp  23541  cmpfi  23546  comppfsc  23670  kgentopon  23676  txcmplem2  23780  filconn  24021  alexsubALTlem3  24187  alexsubALT  24189  ptcmplem3  24192  dyadmbllem  25739  shsupcl  31671  hsupss  31674  shatomistici  32694  carsggect  34689  cvmliftlem15  35771  filnetlem3  36872  ttcmin  36988  dfttc2g  36998  icoreunrn  37986  ctbssinf  38033  pibt2  38044  heiborlem1  38443  lssats  39767  lpssat  39768  lssatle  39770  lssat  39771  dicval  41931  onsupneqmaxlim0  43934  onsupnmax  43938  onsssupeqcond  43990  mreuniss  49661