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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2145   ⊆ wss 3902  ∪ 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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871

This theorem is used by:  unissi  4879  unissd  4880  intssuni2  4936  uniintsn  4948  relfld  6276  dffv2  6977  trcl  9711  cflm  10255  coflim  10267  cfslbn  10273  fin23lem41  10358  fin1a2lem12  10417  tskuni  10796  prdsvallem  17545  prdsval  17546  prdsbas  17548  prdsplusg  17549  prdsmulr  17550  prdsvsca  17551  prdshom  17558  mrcssv  17708  catcfuccl  18213  catcxpccl  18301  mrelatlub  18656  mreclatBAD  18657  dprdres  20163  dmdprdsplit2lem  20180  tgcl  23200  distop  23226  fctop  23235  cctop  23237  neiptoptop  23362  cmpcld  23633  uncmp  23634  cmpfi  23639  comppfsc  23764  kgentopon  23770  txcmplem2  23874  filconn  24115  alexsubALTlem3  24281  alexsubALT  24283  ptcmplem3  24286  dyadmbllem  25833  shsupcl  31827  hsupss  31830  shatomistici  32850  carsggect  34837  cvmliftlem15  35885  filnetlem3  37007  ttcmin  37123  dfttc2g  37133  icoreunrn  38121  ctbssinf  38168  pibt2  38179  heiborlem1  38569  lssats  39893  lpssat  39894  lssatle  39896  lssat  39897  dicval  42057  onsupneqmaxlim0  44073  onsupnmax  44077  onsssupeqcond  44129  mreuniss  49834