Theorem uniss 4858

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851

This theorem is referenced by:  unissi  4859  unissd  4860  intssuni2  4915  uniintsn  4927  relfld  6239  dffv2  6935  trcl  9649  cflm  10172  coflim  10183  cfslbn  10189  fin23lem41  10274  fin1a2lem12  10333  tskuni  10706  prdsvallem  17417  prdsval  17418  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  mrcssv  17580  catcfuccl  18085  catcxpccl  18173  mrelatlub  18528  mreclatBAD  18529  dprdres  20005  dmdprdsplit2lem  20022  tgcl  22934  distop  22960  fctop  22969  cctop  22971  neiptoptop  23096  cmpcld  23367  uncmp  23368  cmpfi  23373  comppfsc  23497  kgentopon  23503  txcmplem2  23607  filconn  23848  alexsubALTlem3  24014  alexsubALT  24016  ptcmplem3  24019  dyadmbllem  25566  shsupcl  31409  hsupss  31412  shatomistici  32432  carsggect  34462  cvmliftlem15  35480  filnetlem3  36562  ttcmin  36678  dfttc2g  36688  icoreunrn  37675  ctbssinf  37722  pibt2  37733  heiborlem1  38132  lssats  39458  lpssat  39459  lssatle  39461  lssat  39462  dicval  41622  onsupneqmaxlim0  43652  onsupnmax  43656  onsssupeqcond  43708  mreuniss  49375