Theorem uniss 4859

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 3916	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 613	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1919	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4854	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4854	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3928	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114   ⊆ wss 3890  ∪ cuni 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852

This theorem is referenced by:  unissi  4860  unissd  4861  intssuni2  4916  uniintsn  4928  relfld  6233  dffv2  6929  trcl  9640  cflm  10163  coflim  10174  cfslbn  10180  fin23lem41  10265  fin1a2lem12  10324  tskuni  10697  prdsvallem  17408  prdsval  17409  prdsbas  17411  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  prdshom  17421  mrcssv  17571  catcfuccl  18076  catcxpccl  18164  mrelatlub  18519  mreclatBAD  18520  dprdres  19996  dmdprdsplit2lem  20013  tgcl  22944  distop  22970  fctop  22979  cctop  22981  neiptoptop  23106  cmpcld  23377  uncmp  23378  cmpfi  23383  comppfsc  23507  kgentopon  23513  txcmplem2  23617  filconn  23858  alexsubALTlem3  24024  alexsubALT  24026  ptcmplem3  24029  dyadmbllem  25576  shsupcl  31424  hsupss  31427  shatomistici  32447  carsggect  34478  cvmliftlem15  35496  filnetlem3  36578  ttcmin  36694  dfttc2g  36704  icoreunrn  37689  ctbssinf  37736  pibt2  37747  heiborlem1  38146  lssats  39472  lpssat  39473  lssatle  39475  lssat  39476  dicval  41636  onsupneqmaxlim0  43670  onsupnmax  43674  onsssupeqcond  43726  mreuniss  49387