Theorem uniss 4896

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109   ⊆ wss 3931  ∪ cuni 4888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-uni 4889

This theorem is referenced by:  unissi  4897  unissd  4898  intssuni2  4954  uniintsn  4966  relfld  6269  dffv2  6979  trcl  9747  cflm  10269  coflim  10280  cfslbn  10286  fin23lem41  10371  fin1a2lem12  10430  tskuni  10802  prdsvallem  17473  prdsval  17474  prdsbas  17476  prdsplusg  17477  prdsmulr  17478  prdsvsca  17479  prdshom  17486  mrcssv  17631  catcfuccl  18136  catcxpccl  18224  mrelatlub  18577  mreclatBAD  18578  dprdres  20016  dmdprdsplit2lem  20033  tgcl  22912  distop  22938  fctop  22947  cctop  22949  neiptoptop  23074  cmpcld  23345  uncmp  23346  cmpfi  23351  comppfsc  23475  kgentopon  23481  txcmplem2  23585  filconn  23826  alexsubALTlem3  23992  alexsubALT  23994  ptcmplem3  23997  dyadmbllem  25557  shsupcl  31324  hsupss  31327  shatomistici  32347  carsggect  34355  cvmliftlem15  35325  filnetlem3  36403  icoreunrn  37382  ctbssinf  37429  pibt2  37440  heiborlem1  37840  lssats  39035  lpssat  39036  lssatle  39038  lssat  39039  dicval  41200  onsupneqmaxlim0  43215  onsupnmax  43219  onsssupeqcond  43271  mreuniss  48841