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

Theorem ssel2 3351
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
Assertion
Ref Expression
ssel2  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )

Proof of Theorem ssel2
StepHypRef Expression
1 ssel 3350 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 429 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756    C_ wss 3328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3335  df-ss 3342
This theorem is referenced by:  tz7.7  4745  onfr  4758  onmindif  4808  ordunisssuc  4821  ssimaex  5756  nssdmovg  6245  onnmin  6414  onmindif2  6423  limsssuc  6461  1st2nd  6620  f1o2ndf1  6680  boxriin  7305  ordunifi  7562  isfinite2  7570  ordtypelem7  7738  sucprcreg  7814  cnfcom  7933  cnfcomOLD  7941  coflim  8430  cflim2  8432  fin23lem11  8486  fin23lem26  8494  fin1a2lem13  8581  fpwwe2lem12  8808  suplem2pr  9222  axpre-sup  9336  axsup  9450  dedekind  9533  dedekindle  9534  lbinfm  10283  dfinfmr  10307  infmrcl  10309  infmrlb  10311  uzwo  10917  uzwoOLD  10918  supminf  10942  lbzbi  10943  zsupss  10944  suprzcl2  10945  xrsupsslem  11269  xrinfmsslem  11270  xrub  11274  supxr2  11276  supxrun  11278  supxrunb1  11282  supxrbnd1  11284  supxrbnd2  11285  supxrub  11287  supxrbnd  11291  infmxrlb  11296  ssfzo12  11620  seqsplit  11839  shftlem  12557  rpnnen2lem10  13506  rpnnen2lem11  13507  gcdcllem1  13695  mrcuni  14559  isacs1i  14595  mreacs  14596  lubss  15291  gsumwspan  15524  subgint  15705  cntziinsn  15852  cntzsubg  15854  pmtrdifellem4  15985  subrgint  16887  cntzsubr  16897  mdetunilem9  18426  tgcl  18574  fctop  18608  cctop  18610  neips  18717  cmpsub  19003  1stcelcls  19065  txbasval  19179  fgss2  19447  filcon  19456  filuni  19458  filssufilg  19484  fmfnfmlem4  19530  trust  19804  elmopn2  20020  metrest  20099  dscopn  20166  metds0  20426  cncfmet  20484  negcncf  20494  iscmet2  20805  ovolfioo  20951  ovolficc  20952  itg1mulc  21182  ply1term  21672  plyconst  21674  reeff1olem  21911  usgraedgrnv  23296  ghsubgolem  23857  ocsh  24686  ocorth  24694  spansncvi  25055  pjss1coi  25567  sumdmdii  25819  dfcnv2  25994  xrge0infss  26053  measres  26636  measdivcstOLD  26638  measdivcst  26639  dya2iocuni  26698  frrlem5e  27776  nobndlem2  27834  nobndlem6  27838  nobndlem8  27840  nobndup  27841  nobnddown  27842  nofulllem3  27845  nofulllem4  27846  nofulllem5  27847  fin2so  28416  opnrebl  28515  opnrebl2  28516  fness  28554  ssref  28555  comppfsc  28579  frinfm  28629  filbcmb  28634  nnubfi  28646  nninfnub  28647  sstotbnd3  28675  bndss  28685  exidreslem  28742  isidlc  28815  idlnegcl  28822  intidl  28829  unichnidl  28831  ssfz12  30197  uhgraedgrnv  30273  suprfinzcl  30745  fsuppmapnn0fiublem  30798  fsuppmapnn0fiub  30799  fsuppmapnn0fiub0  30801  lindslinindimp2lem4  30995  lindslinindsimp2  30997  lincresunit3lem2  31014  lincresunit3  31015  snsslVD  31565  snssl  31566  sstrALT2VD  31570  sstrALT2  31571  suctrALTcf  31658  suctrALTcfVD  31659  bnj1190  31999  pmapglb2N  33415  elpaddn0  33444  paddasslem9  33472  paddasslem10  33473  pclfinN  33544  polval2N  33550  diaglbN  34700  dihord6apre  34901
  Copyright terms: Public domain W3C validator