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

Theorem ssel2 3335
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 3334 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 419 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725    C_ wss 3312
This theorem is referenced by:  tz7.7  4599  onfr  4612  onmindif  4662  ordunisssuc  4675  onnmin  4774  onmindif2  4783  limsssuc  4821  ssimaex  5779  nssdmovg  6220  1st2nd  6384  f1o2ndf1  6445  boxriin  7095  ordunifi  7348  isfinite2  7356  ordtypelem7  7482  cnfcom  7646  coflim  8130  cflim2  8132  fin23lem11  8186  fin23lem26  8194  fin1a2lem13  8281  fpwwe2lem12  8505  suplem2pr  8919  axpre-sup  9033  axsup  9140  lbinfm  9950  dfinfmr  9974  infmrcl  9976  infmrlb  9978  uzwo  10528  uzwoOLD  10529  supminf  10552  lbzbi  10553  zsupss  10554  suprzcl2  10555  xrsupsslem  10874  xrinfmsslem  10875  xrub  10879  supxr2  10881  supxrun  10883  supxrunb1  10887  supxrbnd1  10889  supxrbnd2  10890  supxrub  10892  supxrbnd  10896  infmxrlb  10901  seqsplit  11344  shftlem  11871  rpnnen2lem10  12811  rpnnen2lem11  12812  gcdcllem1  12999  mrcuni  13834  isacs1i  13870  mreacs  13871  lubss  14536  gsumwspan  14779  subgint  14952  cntziinsn  15121  cntzsubg  15123  subrgint  15878  cntzsubr  15888  tgcl  17022  fctop  17056  cctop  17058  neips  17165  cmpsub  17451  1stcelcls  17512  txbasval  17626  fgss2  17894  filcon  17903  filuni  17905  filssufilg  17931  fmfnfmlem4  17977  trust  18247  elmopn2  18463  metrest  18542  dscopn  18609  metds0  18868  cncfmet  18926  negcncf  18936  iscmet2  19235  ovolfioo  19352  ovolficc  19353  itg1mulc  19584  ply1term  20111  plyconst  20113  reeff1olem  20350  usgraedgrnv  21385  ghsubgolem  21946  ocsh  22773  ocorth  22781  spansncvi  23142  pjss1coi  23654  sumdmdii  23906  measres  24564  measdivcstOLD  24566  measdivcst  24567  dya2iocuni  24621  dedekind  25175  dedekindle  25176  tfrALTlem  25531  frrlem5e  25544  nobndlem2  25602  nobndlem6  25606  nobndlem8  25608  nobndup  25609  nobnddown  25610  nofulllem3  25613  nofulllem4  25614  nofulllem5  25615  opnrebl  26260  opnrebl2  26261  fness  26299  ssref  26300  comppfsc  26324  frinfm  26374  filbcmb  26379  nnubfi  26391  nninfnub  26392  sstotbnd3  26422  bndss  26432  exidreslem  26489  isidlc  26562  idlnegcl  26569  intidl  26576  unichnidl  26578  ssfz12  28026  ssfzo12  28042  lswrdshwrd  28152  uhgraedgrnv  28176  snsslVD  28795  snssl  28796  sstrALT2VD  28800  sstrALT2  28801  suctrALTcf  28888  suctrALTcfVD  28889  bnj1190  29231  pmapglb2N  30407  elpaddn0  30436  paddasslem9  30464  paddasslem10  30465  pclfinN  30536  polval2N  30542  diaglbN  31692  dihord6apre  31893
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator