Theorem uniss 4876

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1802   ∈ wcel 2145   ⊆ wss 3907  ∪ cuni 4868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-uni 4869

This theorem is referenced by:  unissi  4877  unissd  4878  intssuni2  4934  uniintsn  4946  relfld  6266  dffv2  6966  trcl  9685  cflm  10221  coflim  10233  cfslbn  10239  fin23lem41  10324  fin1a2lem12  10383  tskuni  10756  prdsvallem  17497  prdsval  17498  prdsbas  17500  prdsplusg  17501  prdsmulr  17502  prdsvsca  17503  prdshom  17510  mrcssv  17660  catcfuccl  18165  catcxpccl  18253  mrelatlub  18608  mreclatBAD  18609  dprdres  20091  dmdprdsplit2lem  20108  tgcl  23087  distop  23113  fctop  23122  cctop  23124  neiptoptop  23249  cmpcld  23520  uncmp  23521  cmpfi  23526  comppfsc  23650  kgentopon  23656  txcmplem2  23760  filconn  24001  alexsubALTlem3  24167  alexsubALT  24169  ptcmplem3  24172  dyadmbllem  25719  shsupcl  31599  hsupss  31602  shatomistici  32622  carsggect  34625  cvmliftlem15  35661  filnetlem3  36753  ttcmin  36869  dfttc2g  36879  icoreunrn  37865  ctbssinf  37912  pibt2  37923  heiborlem1  38322  lssats  39648  lpssat  39649  lssatle  39651  lssat  39652  dicval  41812  onsupneqmaxlim0  43813  onsupnmax  43817  onsssupeqcond  43869  mreuniss  49529