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

Theorem ssel2 3562
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
Assertion
Ref Expression
ssel2 ((𝐴𝐵𝐶𝐴) → 𝐶𝐵)

Proof of Theorem ssel2
StepHypRef Expression
1 ssel 3561 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
21imp 443 1 ((𝐴𝐵𝐶𝐴) → 𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wss 3539
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-in 3546  df-ss 3553
This theorem is referenced by:  tz7.7  5652  onfr  5666  onmindif  5718  ordunisssuc  5733  ssimaex  6158  nssdmovg  6692  onnmin  6873  onmindif2  6882  limsssuc  6920  1st2nd  7083  f1o2ndf1  7150  dfrecs3  7334  boxriin  7814  ordunifi  8073  isfinite2  8081  ordtypelem7  8290  sucprcreg  8367  cnfcom  8458  coflim  8944  cflim2  8946  fin23lem11  9000  fin23lem26  9008  fin1a2lem13  9095  fpwwe2lem12  9320  suplem2pr  9732  axpre-sup  9847  axsup  9965  dedekind  10052  dedekindle  10053  lbinf  10828  dfinfre  10854  infrelb  10858  suprfinzcl  11327  uzwo  11586  supminf  11610  lbzbi  11611  zsupss  11612  suprzcl2  11613  xrsupsslem  11968  xrinfmsslem  11969  xrub  11973  supxr2  11975  supxrun  11977  supxrunb1  11980  supxrbnd1  11982  supxrbnd2  11983  supxrub  11985  supxrbnd  11989  infxrlb  11995  elfzom1elp1fzo  12360  ssfzo12  12385  fsuppmapnn0fiublem  12609  fsuppmapnn0fiub  12610  fsuppmapnn0fiubOLD  12611  fsuppmapnn0fiub0  12613  seqsplit  12654  shftlem  13605  rpnnen2lem10  14740  rpnnen2lem11  14741  gcdcllem1  15008  mrcuni  16053  isacs1i  16090  mreacs  16091  lubss  16893  gsumwspan  17155  subgint  17390  cntziinsn  17539  cntzsubg  17541  pmtrdifellem4  17671  subrgint  18574  cntzsubr  18584  mdetunilem9  20193  tgcl  20532  fctop  20566  cctop  20568  neips  20675  cmpsub  20961  1stcelcls  21022  ssref  21073  comppfsc  21093  txbasval  21167  fgss2  21436  filcon  21445  filuni  21447  filssufilg  21473  fmfnfmlem4  21519  trust  21791  elmopn2  22008  metrest  22087  dscopn  22136  metds0  22409  cncfmet  22467  negcncf  22477  iscmet2  22845  ovolfioo  22988  ovolficc  22989  itg1mulc  23222  ply1term  23709  plyconst  23711  reeff1olem  23949  usgraedgrnv  25700  ocsh  27360  ocorth  27368  spansncvi  27729  pjss1coi  28240  sumdmdii  28492  dfcnv2  28693  xrge0infss  28749  measres  29446  measdivcstOLD  29448  measdivcst  29449  dya2iocuni  29506  bnj1190  30164  frrlem5e  30866  nobndlem2  30926  nobndlem6  30930  nobndlem8  30932  nobndup  30933  nobnddown  30934  nofulllem3  30937  nofulllem4  30938  nofulllem5  30939  opnrebl  31319  opnrebl2  31320  fness  31348  fin2so  32390  matunitlindflem1  32399  poimirlem27  32430  poimir  32436  frinfm  32524  filbcmb  32529  nnubfi  32540  nninfnub  32541  sstotbnd3  32569  bndss  32579  exidreslem  32670  isidlc  32808  idlnegcl  32815  intidl  32822  unichnidl  32824  pmapglb2N  33899  elpaddn0  33928  paddasslem9  33956  paddasslem10  33957  pclfinN  34028  polval2N  34034  diaglbN  35186  dihord6apre  35387  gneispace  37276  snsslVD  37910  snssl  37911  sstrALT2VD  37915  sstrALT2  37916  suctrALTcf  38004  suctrALTcfVD  38005  ssnel  38051  uzwo4  38070  infxrunb2  38349  infxrbnd2  38350  sge0iunmptlemfi  39130  caratheodorylem2  39241  ovnlerp  39276  ssfz12  40198  usgruspgrb  40433  lindslinindimp2lem4  42066  lindslinindsimp2  42068  lincresunit3lem2  42085  lincresunit3  42086
  Copyright terms: Public domain W3C validator