MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniss Structured version   Visualization version   GIF version

Theorem uniss 4649
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.
StepHypRef Expression
1 ssel 3790 . . . . 5 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
21anim2d 606 . . . 4 (𝐴𝐵 → ((𝑥𝑦𝑦𝐴) → (𝑥𝑦𝑦𝐵)))
32eximdv 2013 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝑦𝑦𝐴) → ∃𝑦(𝑥𝑦𝑦𝐵)))
4 eluni 4629 . . 3 (𝑥 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦𝐴))
5 eluni 4629 . . 3 (𝑥 𝐵 ↔ ∃𝑦(𝑥𝑦𝑦𝐵))
63, 4, 53imtr4g 288 . 2 (𝐴𝐵 → (𝑥 𝐴𝑥 𝐵))
76ssrdv 3802 1 (𝐴𝐵 𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wex 1875  wcel 2157  wss 3767   cuni 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-v 3385  df-in 3774  df-ss 3781  df-uni 4627
This theorem is referenced by:  unissi  4651  unissd  4652  intssuni2  4690  uniintsn  4702  relfld  5878  dffv2  6494  trcl  8852  cflm  9358  coflim  9369  cfslbn  9375  fin23lem41  9460  fin1a2lem12  9519  tskuni  9891  prdsval  16427  prdsbas  16429  prdsplusg  16430  prdsmulr  16431  prdsvsca  16432  prdshom  16439  mrcssv  16586  catcfuccl  17070  catcxpccl  17159  mrelatlub  17498  mreclatBAD  17499  dprdres  18740  dmdprdsplit2lem  18757  tgcl  21099  distop  21125  fctop  21134  cctop  21136  neiptoptop  21261  cmpcld  21531  uncmp  21532  cmpfi  21537  comppfsc  21661  kgentopon  21667  txcmplem2  21771  filconn  22012  alexsubALTlem3  22178  alexsubALT  22180  ptcmplem3  22183  dyadmbllem  23704  shsupcl  28714  hsupss  28717  shatomistici  29737  pwuniss  29880  carsggect  30888  carsgclctun  30891  cvmliftlem15  31789  frrlem5c  32291  filnetlem3  32879  icoreunrn  33697  heiborlem1  34089  lssats  35025  lpssat  35026  lssatle  35028  lssat  35029  dicval  37189  pwsal  41266  prsal  41269  intsaluni  41278
  Copyright terms: Public domain W3C validator