Theorem uniss 4939

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 4002	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 611	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1916	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4934	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4934	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 4014	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1777   ∈ wcel 2108   ⊆ wss 3976  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932

This theorem is referenced by:  unissi  4940  unissd  4941  intssuni2  4997  uniintsn  5009  relfld  6306  dffv2  7017  trcl  9797  cflm  10319  coflim  10330  cfslbn  10336  fin23lem41  10421  fin1a2lem12  10480  tskuni  10852  prdsvallem  17514  prdsval  17515  prdsbas  17517  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  prdshom  17527  mrcssv  17672  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  mrelatlub  18632  mreclatBAD  18633  dprdres  20072  dmdprdsplit2lem  20089  tgcl  22997  distop  23023  fctop  23032  cctop  23034  neiptoptop  23160  cmpcld  23431  uncmp  23432  cmpfi  23437  comppfsc  23561  kgentopon  23567  txcmplem2  23671  filconn  23912  alexsubALTlem3  24078  alexsubALT  24080  ptcmplem3  24083  dyadmbllem  25653  shsupcl  31370  hsupss  31373  shatomistici  32393  carsggect  34283  cvmliftlem15  35266  filnetlem3  36346  icoreunrn  37325  ctbssinf  37372  pibt2  37383  heiborlem1  37771  lssats  38968  lpssat  38969  lssatle  38971  lssat  38972  dicval  41133  onsupneqmaxlim0  43185  onsupnmax  43189  onsssupeqcond  43242  mreuniss  48579