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

Theorem ssel2 3913
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 3911 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
21imp 410 1 ((𝐴𝐵𝐶𝐴) → 𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112  wss 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  tz7.7  6189  onfr  6202  onmindif  6252  ordunisssuc  6265  ssimaex  6727  nssdmovg  7314  onnmin  7502  onmindif2  7511  limsssuc  7549  1st2nd  7724  f1o2ndf1  7805  dfrecs3  7996  boxriin  8491  ordunifi  8756  isfinite2  8764  ordtypelem7  8976  sucprcreg  9053  cnfcom  9151  eldju1st  9340  coflim  9676  cflim2  9678  fin23lem11  9732  fin23lem26  9740  fin1a2lem13  9827  fpwwe2lem12  10056  suplem2pr  10468  axpre-sup  10584  axsup  10709  dedekind  10796  dedekindle  10797  fimaxre  11577  fiminre  11580  lbinf  11585  dfinfre  11613  infrelb  11617  suprfinzcl  12089  uzwo  12303  supminf  12327  lbzbi  12328  zsupss  12329  suprzcl2  12330  xrsupsslem  12692  xrinfmsslem  12693  xrub  12697  supxr2  12699  supxrun  12701  supxrunb1  12704  supxrbnd1  12706  supxrbnd2  12707  supxrub  12709  supxrbnd  12713  infxrlb  12719  elfzom1elp1fzo  13103  ssfzo12  13129  fsuppmapnn0fiublem  13357  fsuppmapnn0fiub  13358  fsuppmapnn0fiub0  13360  seqsplit  13403  shftlem  14423  rpnnen2lem10  15572  rpnnen2lem11  15573  gcdcllem1  15842  mrcuni  16888  isacs1i  16924  mreacs  16925  lubss  17727  gsumwspan  18007  subgint  18299  cntziinsn  18461  cntzsubg  18463  pmtrdifellem4  18603  subrgint  19554  cntzsubr  19565  mdetunilem9  21229  tgcl  21578  fctop  21613  cctop  21615  neips  21722  cmpsub  22009  1stcelcls  22070  ssref  22121  comppfsc  22141  txbasval  22215  fgss2  22483  filconn  22492  filuni  22494  filssufilg  22520  fmfnfmlem4  22566  trust  22839  elmopn2  23056  metrest  23135  dscopn  23184  metds0  23459  cncfmet  23518  negcncf  23531  iscmet2  23902  ovolfioo  24075  ovolficc  24076  itg1mulc  24312  ply1term  24805  plyconst  24807  reeff1olem  25045  usgruspgrb  26978  ocsh  29070  ocorth  29078  spansncvi  29439  pjss1coi  29950  sumdmdii  30202  unidifsnel  30311  dfcnv2  30443  xrge0infss  30514  measdivcst  31597  measdivcstALTV  31598  dya2iocuni  31655  bnj1190  32394  nosupno  33317  nosupbday  33319  nosupbnd1lem5  33326  noetalem3  33333  opnrebl  33782  opnrebl2  33783  fness  33811  nlpineqsn  34826  fin2so  35043  matunitlindflem1  35052  poimirlem27  35083  poimir  35089  frinfm  35172  filbcmb  35177  nnubfi  35187  nninfnub  35188  sstotbnd3  35213  bndss  35223  exidreslem  35314  isidlc  35452  idlnegcl  35459  intidl  35466  unichnidl  35468  pmapglb2N  37066  elpaddn0  37095  paddasslem9  37123  paddasslem10  37124  pclfinN  37195  polval2N  37201  diaglbN  38350  dihord6apre  38551  gneispace  40830  snsslVD  41528  snssl  41529  sstrALT2VD  41533  sstrALT2  41534  suctrALTcf  41621  suctrALTcfVD  41622  ssnel  41667  uzwo4  41680  infxrunb2  41993  infxrbnd2  41994  supxrunb3  42029  unb2ltle  42045  infxrpnf  42077  supminfxr  42096  sge0iunmptlemfi  43045  caratheodorylem2  43159  ovnlerp  43194  ssfz12  43864  prssspr  43995  prsssprel  43998  lindslinindimp2lem4  44863  lindslinindsimp2  44865  lincresunit3lem2  44882  lincresunit3  44883
  Copyright terms: Public domain W3C validator