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

Theorem uniss 4566
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 3703 . . . . 5 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
21anim2d 590 . . . 4 (𝐴𝐵 → ((𝑥𝑦𝑦𝐴) → (𝑥𝑦𝑦𝐵)))
32eximdv 1959 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝑦𝑦𝐴) → ∃𝑦(𝑥𝑦𝑦𝐵)))
4 eluni 4547 . . 3 (𝑥 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦𝐴))
5 eluni 4547 . . 3 (𝑥 𝐵 ↔ ∃𝑦(𝑥𝑦𝑦𝐵))
63, 4, 53imtr4g 285 . 2 (𝐴𝐵 → (𝑥 𝐴𝑥 𝐵))
76ssrdv 3715 1 (𝐴𝐵 𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wex 1817  wcel 2103  wss 3680   cuni 4544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-in 3687  df-ss 3694  df-uni 4545
This theorem is referenced by:  unissi  4569  unissd  4570  intssuni2  4610  uniintsn  4622  relfld  5774  dffv2  6385  trcl  8717  cflm  9185  coflim  9196  cfslbn  9202  fin23lem41  9287  fin1a2lem12  9346  tskuni  9718  prdsval  16238  prdsbas  16240  prdsplusg  16241  prdsmulr  16242  prdsvsca  16243  prdshom  16250  mrcssv  16397  catcfuccl  16881  catcxpccl  16969  mrelatlub  17308  mreclatBAD  17309  dprdres  18548  dmdprdsplit2lem  18565  tgcl  20896  distop  20922  fctop  20931  cctop  20933  neiptoptop  21058  cmpcld  21328  uncmp  21329  cmpfi  21334  comppfsc  21458  kgentopon  21464  txcmplem2  21568  filconn  21809  alexsubALTlem3  21975  alexsubALT  21977  ptcmplem3  21980  dyadmbllem  23488  shsupcl  28427  hsupss  28430  shatomistici  29450  pwuniss  29598  carsggect  30610  carsgclctun  30613  cvmliftlem15  31508  frrlem5c  32013  filnetlem3  32602  icoreunrn  33439  heiborlem1  33842  lssats  34719  lpssat  34720  lssatle  34722  lssat  34723  dicval  36884  pwsal  40955  prsal  40958  intsaluni  40967
  Copyright terms: Public domain W3C validator