Theorem uniss 4873

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 3937	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 612	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1920	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4868	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4868	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 295	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3950	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1781   ∈ wcel 2106   ⊆ wss 3910  ∪ cuni 4865

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-in 3917  df-ss 3927  df-uni 4866

This theorem is referenced by:  unissi  4874  unissd  4875  intssuni2  4934  uniintsn  4948  relfld  6227  dffv2  6936  trcl  9664  cflm  10186  coflim  10197  cfslbn  10203  fin23lem41  10288  fin1a2lem12  10347  tskuni  10719  prdsvallem  17336  prdsval  17337  prdsbas  17339  prdsplusg  17340  prdsmulr  17341  prdsvsca  17342  prdshom  17349  mrcssv  17494  catcfuccl  18005  catcfucclOLD  18006  catcxpccl  18095  catcxpcclOLD  18096  mrelatlub  18451  mreclatBAD  18452  dprdres  19807  dmdprdsplit2lem  19824  tgcl  22319  distop  22345  fctop  22354  cctop  22356  neiptoptop  22482  cmpcld  22753  uncmp  22754  cmpfi  22759  comppfsc  22883  kgentopon  22889  txcmplem2  22993  filconn  23234  alexsubALTlem3  23400  alexsubALT  23402  ptcmplem3  23405  dyadmbllem  24963  shsupcl  30280  hsupss  30283  shatomistici  31303  carsggect  32918  cvmliftlem15  33892  filnetlem3  34852  icoreunrn  35830  ctbssinf  35877  pibt2  35888  heiborlem1  36270  lssats  37474  lpssat  37475  lssatle  37477  lssat  37478  dicval  39639  onsupneqmaxlim0  41544  onsupnmax  41548  onsssupeqcond  41601  mreuniss  46922