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

Theorem uniss 4388
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 3561 . . . . 5 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
21anim2d 586 . . . 4 (𝐴𝐵 → ((𝑥𝑦𝑦𝐴) → (𝑥𝑦𝑦𝐵)))
32eximdv 1832 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝑦𝑦𝐴) → ∃𝑦(𝑥𝑦𝑦𝐵)))
4 eluni 4369 . . 3 (𝑥 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦𝐴))
5 eluni 4369 . . 3 (𝑥 𝐵 ↔ ∃𝑦(𝑥𝑦𝑦𝐵))
63, 4, 53imtr4g 283 . 2 (𝐴𝐵 → (𝑥 𝐴𝑥 𝐵))
76ssrdv 3573 1 (𝐴𝐵 𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wex 1694  wcel 1976  wss 3539   cuni 4366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553  df-uni 4367
This theorem is referenced by:  unissi  4391  unissd  4392  intssuni2  4431  uniintsn  4443  relfld  5564  dffv2  6166  trcl  8464  cflm  8932  coflim  8943  cfslbn  8949  fin23lem41  9034  fin1a2lem12  9093  tskuni  9461  prdsval  15884  prdsbas  15886  prdsplusg  15887  prdsmulr  15888  prdsvsca  15889  prdshom  15896  mrcssv  16043  catcfuccl  16528  catcxpccl  16616  mrelatlub  16955  mreclatBAD  16956  dprdres  18196  dmdprdsplit2lem  18213  tgcl  20526  distop  20552  fctop  20560  cctop  20562  neiptoptop  20687  cmpcld  20957  uncmp  20958  cmpfi  20963  comppfsc  21087  kgentopon  21093  txcmplem2  21197  filcon  21439  alexsubALTlem3  21605  alexsubALT  21607  ptcmplem3  21610  dyadmbllem  23090  shsupcl  27387  hsupss  27390  shatomistici  28410  pwuniss  28559  carsggect  29513  carsgclctun  29516  cvmliftlem15  30340  frrlem5c  30836  filnetlem3  31351  icoreunrn  32179  heiborlem1  32576  lssats  33113  lpssat  33114  lssatle  33116  lssat  33117  dicval  35279  pwsal  39008  prsal  39011  intsaluni  39020
  Copyright terms: Public domain W3C validator