Theorem uniss 4871

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2113   ⊆ wss 3901  ∪ cuni 4863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-uni 4864

This theorem is referenced by:  unissi  4872  unissd  4873  intssuni2  4928  uniintsn  4940  relfld  6233  dffv2  6929  trcl  9637  cflm  10160  coflim  10171  cfslbn  10177  fin23lem41  10262  fin1a2lem12  10321  tskuni  10694  prdsvallem  17374  prdsval  17375  prdsbas  17377  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  prdshom  17387  mrcssv  17537  catcfuccl  18042  catcxpccl  18130  mrelatlub  18485  mreclatBAD  18486  dprdres  19959  dmdprdsplit2lem  19976  tgcl  22913  distop  22939  fctop  22948  cctop  22950  neiptoptop  23075  cmpcld  23346  uncmp  23347  cmpfi  23352  comppfsc  23476  kgentopon  23482  txcmplem2  23586  filconn  23827  alexsubALTlem3  23993  alexsubALT  23995  ptcmplem3  23998  dyadmbllem  25556  shsupcl  31413  hsupss  31416  shatomistici  32436  carsggect  34475  cvmliftlem15  35492  filnetlem3  36574  icoreunrn  37560  ctbssinf  37607  pibt2  37618  heiborlem1  38008  lssats  39268  lpssat  39269  lssatle  39271  lssat  39272  dicval  41432  onsupneqmaxlim0  43462  onsupnmax  43466  onsssupeqcond  43518  mreuniss  49141