Theorem uniss 4885

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2146   ⊆ wss 3908  ∪ cuni 4877

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-uni 4878

This theorem is used by:  unissi  4886  unissd  4887  intssuni2  4943  uniintsn  4955  relfld  6282  dffv2  6983  trcl  9707  cflm  10251  coflim  10263  cfslbn  10269  fin23lem41  10354  fin1a2lem12  10413  tskuni  10786  prdsvallem  17532  prdsval  17533  prdsbas  17535  prdsplusg  17536  prdsmulr  17537  prdsvsca  17538  prdshom  17545  mrcssv  17695  catcfuccl  18200  catcxpccl  18288  mrelatlub  18643  mreclatBAD  18644  dprdres  20131  dmdprdsplit2lem  20148  tgcl  23163  distop  23189  fctop  23198  cctop  23200  neiptoptop  23325  cmpcld  23596  uncmp  23597  cmpfi  23602  comppfsc  23726  kgentopon  23732  txcmplem2  23836  filconn  24077  alexsubALTlem3  24243  alexsubALT  24245  ptcmplem3  24248  dyadmbllem  25795  shsupcl  31727  hsupss  31730  shatomistici  32750  carsggect  34740  cvmliftlem15  35811  filnetlem3  36932  ttcmin  37048  dfttc2g  37058  icoreunrn  38046  ctbssinf  38093  pibt2  38104  heiborlem1  38503  lssats  39827  lpssat  39828  lssatle  39830  lssat  39831  dicval  41991  onsupneqmaxlim0  43992  onsupnmax  43996  onsssupeqcond  44048  mreuniss  49719