Theorem uniss 4917

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 3976	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 613	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1921	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4912	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4912	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3989	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 397  ∃wex 1782   ∈ wcel 2107   ⊆ wss 3949  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910

This theorem is referenced by:  unissi  4918  unissd  4919  intssuni2  4978  uniintsn  4992  relfld  6275  dffv2  6987  trcl  9723  cflm  10245  coflim  10256  cfslbn  10262  fin23lem41  10347  fin1a2lem12  10406  tskuni  10778  prdsvallem  17400  prdsval  17401  prdsbas  17403  prdsplusg  17404  prdsmulr  17405  prdsvsca  17406  prdshom  17413  mrcssv  17558  catcfuccl  18069  catcfucclOLD  18070  catcxpccl  18159  catcxpcclOLD  18160  mrelatlub  18515  mreclatBAD  18516  dprdres  19898  dmdprdsplit2lem  19915  tgcl  22472  distop  22498  fctop  22507  cctop  22509  neiptoptop  22635  cmpcld  22906  uncmp  22907  cmpfi  22912  comppfsc  23036  kgentopon  23042  txcmplem2  23146  filconn  23387  alexsubALTlem3  23553  alexsubALT  23555  ptcmplem3  23558  dyadmbllem  25116  shsupcl  30591  hsupss  30594  shatomistici  31614  carsggect  33317  cvmliftlem15  34289  filnetlem3  35265  icoreunrn  36240  ctbssinf  36287  pibt2  36298  heiborlem1  36679  lssats  37882  lpssat  37883  lssatle  37885  lssat  37886  dicval  40047  onsupneqmaxlim0  41973  onsupnmax  41977  onsssupeqcond  42030  mreuniss  47532