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

Theorem sseli 3347
Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sseli.1  |-  A  C_  B
Assertion
Ref Expression
sseli  |-  ( C  e.  A  ->  C  e.  B )

Proof of Theorem sseli
StepHypRef Expression
1 sseli.1 . 2  |-  A  C_  B
2 ssel 3345 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
31, 2ax-mp 5 1  |-  ( C  e.  A  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3323
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 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  sselii  3348  sseldi  3349  elun1  3518  elun2  3519  copsex2ga  4946  issref  5206  2elresin  5517  nfvres  5715  fvco4i  5764  fvmptss  5777  fvmptex  5779  fvmptnf  5786  fvopab4ndm  5789  fvimacnvi  5812  elpreima  5818  iinpreima  5828  ofrfval  6323  ofval  6324  off  6329  nnon  6477  finds  6497  finds2  6499  offres  6567  eqopi  6605  op1steq  6613  dfoprab4  6626  bropopvvv  6648  curry1val  6660  curry2val  6664  reldmtpos  6748  smores3  6806  smores2  6807  frsuc  6884  nnfi  7495  unifpw  7606  f1opwfi  7607  fival  7654  fi0  7662  dffi2  7665  elfiun  7672  cantnfp1lem1  7878  cantnfp1lem3  7880  cantnfp1lem1OLD  7904  cantnfp1lem3OLD  7906  epfrs  7943  r1fin  7972  r1tr  7975  r1ordg  7977  r1ord3g  7978  r1val1  7985  tz9.12lem3  7988  tcrank  8083  cplem1  8088  hta  8096  tskwe  8112  cardprclem  8141  r0weon  8171  fodomfi2  8222  alephfplem3  8268  dfac12r  8307  ackbij1lem6  8386  ackbij1lem9  8389  ackbij1lem10  8390  ackbij1lem11  8391  ackbij1lem16  8396  ackbij1lem18  8398  ackbij2  8404  fin23lem24  8483  fin23lem26  8486  fin23lem28  8501  fin23lem30  8503  fin23lem31  8504  isfin1-3  8547  fin1a2lem6  8566  hsmexlem4  8590  hsmexlem5  8591  hsmexlem6  8592  axdc2lem  8609  axdc3lem2  8612  axcclem  8618  ac6num  8640  brdom5  8688  brdom4  8689  canthp1lem2  8812  r1tskina  8941  gruina  8977  grur1a  8978  pinn  9039  0nnq  9085  elpqn  9086  recn  9364  rexr  9421  dedekindle  9526  ltord1  9858  leord1  9859  eqord1  9860  nnre  10321  nncn  10322  nnind  10332  nnnn0  10578  nn0re  10580  nn0cn  10581  nnz  10660  nn0z  10661  nnq  10958  qcn  10959  rpre  10989  difreicc  11409  iccshftri  11412  iccshftli  11414  iccdili  11416  icccntri  11418  fzval2  11432  fzelp1  11499  4fvwrd4  11525  elfzo1  11587  expcllem  11868  expcl2lem  11869  m1expcl2  11879  bcm1k  12083  bcpasc  12089  hashbclem  12197  swrd0fv0  12328  swrd0fvlsw  12331  seqshft  12566  sqrlem5  12728  cau3lem  12834  caubnd  12838  climconst2  13018  rlimres  13028  lo1res  13029  lo1resb  13034  rlimresb  13035  o1resb  13036  o1of2  13082  o1rlimmul  13088  caurcvg  13146  caucvg  13148  ackbijnn  13283  binomlem  13284  incexclem  13291  divalglem8  13596  sadadd  13655  smueqlem  13678  smumul  13681  isprm3  13764  phimullem  13846  prmdiveq  13853  unbenlem  13961  prmreclem2  13970  prmrec  13975  vdwnnlem1  14048  vdwnnlem3  14050  ramtcl2  14064  cshwshashlem1  14114  isstruct2  14175  structcnvcnv  14177  fvsetsid  14191  strlemor1  14257  imasdsval2  14446  xpsfrnel2  14495  mreunirn  14531  mrcfval  14538  mrisval  14560  isacs2  14583  acsfn  14589  homarcl  14888  arwval  14903  coafval  14924  coapm  14931  isdrs2  15101  isacs3lem  15328  psssdm2  15377  tsrss  15385  submnd0  15443  nmzsubg  15713  nmznsg  15716  resscntz  15840  cntzmhm  15847  symgtrinv  15969  pmtrdifellem4  15976  psgnpmtr  16007  efginvrel2  16215  efginvrel1  16216  efgsp1  16225  efgsres  16226  efgsfo  16227  frgpinv  16252  frgpupf  16261  frgpup1  16263  subcmn  16312  torsubg  16327  dprd2dlem1  16528  dpjidcl  16545  dpjidclOLD  16552  ablfaclem3  16576  subrgpropd  16877  lssacs  17025  sralmod  17245  psrbaglefi  17418  psrbaglefiOLD  17419  mplsubglem  17487  mplsubglemOLD  17489  ressmpladd  17513  ressmplmul  17514  ressmplvsca  17515  mplmonmul  17520  mplind  17559  ply1bascl  17634  cnsubdrglem  17839  rege0subm  17844  rge0srg  17857  zringunit  17889  zrngunit  17890  znrrg  17973  psgnghm  17985  zrhpsgnevpm  17996  evpmodpmf1o  18001  pmtrodpm  18002  frlmsslsp  18198  frlmsslspOLD  18199  islinds4  18239  lmimlbs  18240  lbslcic  18245  mdetralt  18389  mdetunilem7  18399  basdif0  18533  tgval2  18536  mreclatdemoBAD  18675  ordtbas  18771  ordtrest  18781  ordtrestixx  18801  fincmp  18971  cmpfi  18986  bwth  18988  iuncon  19007  1stcrest  19032  hauslly  19071  kgentop  19090  ptbasin  19125  ptcnplem  19169  txkgen  19200  infil  19411  filunirn  19430  uzrest  19445  elflim  19519  hauspwpwf1  19535  flffval  19537  fclsval  19556  isfcls  19557  fcfval  19581  alexsubALTlem3  19596  alexsubALTlem4  19597  ustn0  19770  fmucndlem  19841  xmetunirn  19887  blbas  19980  blres  19981  mopnval  19988  setsmstopn  20028  tmsval  20031  tngtopn  20211  qtopbaslem  20312  xrtgioo  20358  reperflem  20370  icccmplem1  20374  reconnlem2  20379  xrge0tsms  20386  icopnfhmeo  20490  icccvx  20497  bndth  20505  reparphti  20544  pcofval  20557  pcoval1  20560  pcoval2  20563  pcoass  20571  pcorevlem  20573  pcorev2  20575  pi1xfrcnv  20604  nmhmcn  20650  csscld  20736  cfilfval  20750  caufval  20761  cfilres  20782  bcthlem1  20810  ivthlem1  20910  ivthlem3  20912  ovolicc2lem3  20977  ovolicc2lem4  20978  ioombl1lem4  21017  vitalilem1  21063  mbflimsup  21119  i1fima2  21132  i1fd  21134  i1f0  21140  i1f1  21143  itg1addlem4  21152  itg1addlem5  21153  itg2cnlem2  21215  iblmbf  21220  ellimc2  21327  limcres  21336  limcun  21345  dvbsss  21352  perfdvf  21353  dvres2lem  21360  dvaddbr  21387  rolle  21437  cmvth  21438  dvlip  21440  dvlipcn  21441  dvle  21454  lhop1lem  21460  dvfsumle  21468  dvfsumge  21469  dvfsumabs  21470  dvfsumlem2  21474  ftc2  21491  itgparts  21494  itgsubstlem  21495  itgsubst  21496  deg1mul3  21562  coeval  21666  coeeu  21668  dgrval  21671  coef3  21675  coemulc  21697  dgrsub  21714  coecj  21720  dvply2  21727  dvnply  21729  quotval  21733  fta1  21749  plyexmo  21754  aacjcl  21768  taylfval  21799  dvtaylp  21810  abelth  21881  pilem2  21892  pilem3  21893  sinord  21965  recosf1o  21966  resinf1o  21967  tanord1  21968  eff1olem  21979  dvloglem  22068  dvlog  22071  dvlog2lem  22072  advlogexp  22075  logtayl  22080  logtayl2  22082  cxpcn3lem  22160  cxpcn3  22161  sqrcn  22163  loglesqr  22171  1cubr  22212  acosrecl  22273  rlimcnp2  22335  xrlimcnp  22337  efrlim  22338  jensen  22357  basellem4  22396  ppiprm  22464  chtprm  22466  prmorcht  22491  dvdsflip  22497  musum  22506  chpchtsum  22533  dchrinvcl  22567  dchrghm  22570  dchrinv  22575  dchrsum2  22582  dchrsum  22583  rplogsumlem2  22709  rpvmasumlem  22711  dchrisum0re  22737  dchrisum0lem2a  22741  dirith2  22752  pnt  22838  tglng  22955  axlowdimlem5  23143  axlowdimlem6  23144  axlowdimlem7  23145  axlowdimlem15  23153  axlowdimlem16  23154  axlowdimlem17  23155  axlowdim  23158  axeuclidlem  23159  axcontlem2  23162  axcontlem7  23167  axcontlem8  23168  issubgoi  23748  opidon  23760  flddivrng  23853  rngosn3  23864  vcoprnelem  23907  nvvcop  23923  nvex  23940  phnv  24165  sheli  24567  cheli  24586  choc1  24681  shintcli  24683  chintcli  24685  shsleji  24724  pjini  25053  mayete3i  25082  mayete3iOLD  25083  dmadjop  25243  nlelshi  25415  cnlnadjeui  25432  cnlnssadj  25435  bdopadj  25437  pjimai  25531  stcl  25571  atelch  25699  disjin  25880  fcnvgreu  25942  partfun  25944  f1od2  25975  fcobijfs  25977  xrge0infss  26004  iundisj2fi  26032  nnindf  26040  eliccioo  26057  xrsmulgzz  26090  xrge0mulgnn0  26101  xrge0nre  26104  xrge0omnd  26125  xrge0tsmsd  26204  prsdm  26296  prsrn  26297  ordtrestNEW  26303  xrge0iifcnv  26315  xrge0iifcv  26316  xrge0iifiso  26317  xrge0iifhom  26319  qqhcn  26372  rnlogblem  26410  esumval  26452  gsumesum  26462  esumlub  26463  esumcst  26466  esumfsup  26471  issgon  26518  elrnsiga  26521  imambfm  26629  br2base  26636  sxbrsigalem0  26638  dya2iocucvr  26651  sxbrsigalem2  26653  sxbrsigalem5  26655  sxbrsiga  26657  sibfof  26678  oddpwdc  26689  eulerpartlemelr  26692  eulerpartgbij  26707  eulerpartlemgvv  26711  eulerpartlemgh  26713  eulerpartlemgs2  26715  eulerpartlemn  26716  sseqf  26727  ballotlem2  26823  ballotlemfp1  26826  ballotlemfc0  26827  ballotlemfcc  26828  ballotlemfmpn  26829  ballotlemsup  26839  ballotlemfrceq  26863  signswch  26914  lgamgulmlem2  26968  lgamucov2  26977  subfacp1lem5  27024  cvmsi  27106  divcnvshft  27349  zprod  27401  risefaccllem  27467  fallfaccllem  27468  dfon2lem4  27550  wfrlem4  27678  wfrlem10  27684  frrlem4  27722  pprodss4v  27866  linedegen  28125  bpolydiflem  28148  bpoly4  28153  nnssi2  28253  nnssi3  28254  sin2h  28375  cos2h  28376  tan2h  28377  heicant  28379  mblfinlem1  28381  cnambfre  28393  dvtan  28395  itg2addnc  28399  itg2gt0cn  28400  ftc1cnnc  28419  ftc2nc  28429  dvcncxp1  28430  dvcnsqr  28431  dvasin  28433  dvacos  28434  ivthALT  28483  neibastop2lem  28534  cover2  28560  opelopab3  28563  sstotbnd2  28626  heibor1lem  28661  heiborlem10  28672  exidcl  28694  elrfi  28983  elrfirn  28984  elrfirn2  28985  mrefg3  28997  diophin  29064  diophun  29065  eq0rabdioph  29068  eqrabdioph  29069  pellex  29129  rmxycomplete  29211  rmxypos  29243  ltrmynn0  29244  jm2.23  29298  aomclem2  29361  fglmod  29379  lsmfgcl  29380  lmhmfgima  29390  lmhmfgsplit  29392  isnumbasabl  29415  dgrsub2  29444  itgocn  29474  acsfn1p  29509  areaquad  29545  itgsin0pilem1  29743  itgsinexplem1  29747  itgsinexp  29748  stoweidlem34  29782  stoweidlem41  29789  stoweidlem51  29799  wallispilem2  29814  stirlinglem11  29832  elfvmptrab1  30107  2wlkonot3v  30347  2spthonot3v  30348  clwwlknprop  30388  clwwisshclww  30424  onfrALTlem2  31141  onfrALTlem2VD  31512  bnj1533  31732  bnj1137  31873  bnj1286  31897  bnj1408  31914  bnj1417  31919  bj-sngltagi  32322  bj-elid  32368  bj-flbi3  32374  bj-vecmoda  32420  bj-abelcmnda  32423  bj-rrveccmnda  32431  toycom  32458  osumcllem7N  33446  pexmidlem4N  33457  diaintclN  34543  dibintclN  34652  mapd1o  35133  hdmapevec  35323  taupilemrplb  35454
  Copyright terms: Public domain W3C validator