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

Theorem uniss 4858
 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 3965 . . . . 5 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
21anim2d 611 . . . 4 (𝐴𝐵 → ((𝑥𝑦𝑦𝐴) → (𝑥𝑦𝑦𝐵)))
32eximdv 1911 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝑦𝑦𝐴) → ∃𝑦(𝑥𝑦𝑦𝐵)))
4 eluni 4840 . . 3 (𝑥 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦𝐴))
5 eluni 4840 . . 3 (𝑥 𝐵 ↔ ∃𝑦(𝑥𝑦𝑦𝐵))
63, 4, 53imtr4g 297 . 2 (𝐴𝐵 → (𝑥 𝐴𝑥 𝐵))
76ssrdv 3977 1 (𝐴𝐵 𝐴 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1773   ∈ wcel 2107   ⊆ wss 3940  ∪ cuni 4837 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-in 3947  df-ss 3956  df-uni 4838 This theorem is referenced by:  unissi  4860  unissd  4861  intssuni2  4899  uniintsn  4911  relfld  6125  dffv2  6755  trcl  9164  cflm  9666  coflim  9677  cfslbn  9683  fin23lem41  9768  fin1a2lem12  9827  tskuni  10199  prdsval  16723  prdsbas  16725  prdsplusg  16726  prdsmulr  16727  prdsvsca  16728  prdshom  16735  mrcssv  16880  catcfuccl  17364  catcxpccl  17452  mrelatlub  17791  mreclatBAD  17792  dprdres  19086  dmdprdsplit2lem  19103  tgcl  21512  distop  21538  fctop  21547  cctop  21549  neiptoptop  21674  cmpcld  21945  uncmp  21946  cmpfi  21951  comppfsc  22075  kgentopon  22081  txcmplem2  22185  filconn  22426  alexsubALTlem3  22592  alexsubALT  22594  ptcmplem3  22597  dyadmbllem  24134  shsupcl  29048  hsupss  29051  shatomistici  30071  pwuniss  30239  carsggect  31481  carsgclctun  31484  cvmliftlem15  32448  filnetlem3  33631  icoreunrn  34528  ctbssinf  34575  pibt2  34586  heiborlem1  34976  lssats  36034  lpssat  36035  lssatle  36037  lssat  36038  dicval  38198  pwsal  42485  intsaluni  42497
 Copyright terms: Public domain W3C validator