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

Theorem sseli 3346
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 3344 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
31, 2ax-mp 8 1  |-  ( C  e.  A  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726    C_ wss 3322
This theorem is referenced by:  sselii  3347  sseldi  3348  elun1  3516  elun2  3517  nnon  4853  finds  4873  finds2  4875  issref  5249  2elresin  5558  nfvres  5762  fvco4i  5803  fvmptss  5815  fvmptex  5817  fvmptnf  5824  fvopab4ndm  5827  fvimacnvi  5846  elpreima  5852  iinpreima  5862  ofrfval  6315  ofval  6316  offres  6321  off  6322  eqopi  6385  op1steq  6393  dfoprab4  6406  copsex2ga  6410  bropopvvv  6428  curry1val  6441  curry2val  6445  reldmtpos  6489  smores3  6617  smores2  6618  frsuc  6696  nnfi  7301  unifpw  7411  f1opwfi  7412  fival  7419  fi0  7427  dffi2  7430  elfiun  7437  cantnfp1lem1  7636  cantnfp1lem3  7638  epfrs  7669  r1fin  7701  r1tr  7704  r1ordg  7706  r1ord3g  7707  r1val1  7714  tz9.12lem3  7717  tcrank  7810  cplem1  7815  hta  7823  tskwe  7839  cardprclem  7868  r0weon  7896  fodomfi2  7943  alephfplem3  7989  dfac12r  8028  ackbij1lem6  8107  ackbij1lem9  8110  ackbij1lem10  8111  ackbij1lem11  8112  ackbij1lem16  8117  ackbij1lem18  8119  ackbij2  8125  fin23lem24  8204  fin23lem26  8207  fin23lem28  8222  fin23lem30  8224  fin23lem31  8225  isfin1-3  8268  fin1a2lem6  8287  hsmexlem4  8311  hsmexlem5  8312  hsmexlem6  8313  axdc2lem  8330  axdc3lem2  8333  axcclem  8339  ac6num  8361  brdom5  8409  brdom4  8410  canthp1lem2  8530  r1tskina  8659  gruina  8695  grur1a  8696  pinn  8757  0nnq  8803  elpqn  8804  recn  9082  rexr  9132  ltord1  9555  leord1  9556  eqord1  9557  nnre  10009  nncn  10010  nnind  10020  nnnn0  10230  nn0re  10232  nn0cn  10233  nnz  10305  nn0z  10306  nnq  10589  qcn  10590  rpre  10620  difreicc  11030  iccshftri  11033  iccshftli  11035  iccdili  11037  icccntri  11039  fzval2  11048  fzelp1  11101  4fvwrd4  11123  elfzo1  11175  expcllem  11394  expcl2lem  11395  m1expcl2  11405  bcm1k  11608  bcpasc  11614  hashbclem  11703  seqshft  11902  sqrlem5  12054  cau3lem  12160  caubnd  12164  climconst2  12344  rlimres  12354  lo1res  12355  lo1resb  12360  rlimresb  12361  o1resb  12362  o1of2  12408  o1rlimmul  12414  caurcvg  12472  caucvg  12474  zsum  12514  ackbijnn  12609  binomlem  12610  incexclem  12618  divalglem8  12922  sadadd  12981  smueqlem  13004  smumul  13007  isprm3  13090  phimullem  13170  prmdiveq  13177  unbenlem  13278  prmreclem2  13287  prmrec  13292  vdwnnlem1  13365  vdwnnlem3  13367  ramtcl2  13381  isstruct2  13480  structcnvcnv  13482  strlemor1  13558  imasdsval2  13744  xpsfrnel2  13792  mreunirn  13828  mrcfval  13835  mrisval  13857  isacs2  13880  acsfn  13886  homarcl  14185  arwval  14200  coafval  14221  coapm  14228  isdrs2  14398  isacs3lem  14594  psssdm2  14649  tsrss  14657  submnd0  14727  nmzsubg  14983  nmznsg  14986  resscntz  15132  cntzmhm  15139  efginvrel2  15361  efginvrel1  15362  efgsp1  15371  efgsres  15372  efgsfo  15373  frgpinv  15398  frgpupf  15407  frgpup1  15409  subcmn  15458  torsubg  15471  dprd2dlem1  15601  dpjidcl  15618  ablfaclem3  15647  subrgpropd  15904  lssacs  16045  sralmod  16260  psrbaglefi  16439  mplsubglem  16500  ressmpladd  16522  ressmplmul  16523  ressmplvsca  16524  mplmonmul  16529  mplind  16564  ply1bascl  16603  cnsubdrglem  16751  rege0subm  16757  zrngunit  16767  znrrg  16848  basdif0  17020  tgval2  17023  mreclatdemo  17162  ordtbas  17258  ordtrest  17268  ordtrestixx  17288  fincmp  17458  cmpfi  17473  iuncon  17493  1stcrest  17518  hauslly  17557  kgentop  17576  ptbasin  17611  ptcnplem  17655  txkgen  17686  infil  17897  filunirn  17916  uzrest  17931  elflim  18005  hauspwpwf1  18021  flffval  18023  fclsval  18042  isfcls  18043  fcfval  18067  alexsubALTlem3  18082  alexsubALTlem4  18083  ustn0  18252  fmucndlem  18323  xmetunirn  18369  blbas  18462  blres  18463  mopnval  18470  setsmstopn  18510  tmsval  18513  tngtopn  18693  qtopbaslem  18794  xrtgioo  18839  reperflem  18851  icccmplem1  18855  reconnlem2  18860  xrge0tsms  18867  icopnfhmeo  18970  icccvx  18977  bndth  18985  reparphti  19024  pcofval  19037  pcoval1  19040  pcoval2  19043  pcoass  19051  pcorevlem  19053  pcorev2  19055  pi1xfrcnv  19084  nmhmcn  19130  csscld  19205  cfilfval  19219  caufval  19230  cfilres  19251  bcthlem1  19279  ivthlem1  19350  ivthlem3  19352  ovolicc2lem3  19417  ovolicc2lem4  19418  ioombl1lem4  19457  vitalilem1  19502  mbflimsup  19560  i1fima2  19573  i1fd  19575  i1f0  19581  i1f1  19584  itg1addlem4  19593  itg1addlem5  19594  itg2cnlem2  19656  iblmbf  19661  ellimc2  19766  limcres  19775  limcun  19784  dvbsss  19791  perfdvf  19792  dvres2lem  19799  dvaddbr  19826  rolle  19876  cmvth  19877  dvlip  19879  dvlipcn  19880  dvle  19893  lhop1lem  19899  dvfsumle  19907  dvfsumge  19908  dvfsumabs  19909  dvfsumlem2  19913  ftc2  19930  itgparts  19933  itgsubstlem  19934  itgsubst  19935  deg1mul3  20040  coeval  20144  coeeu  20146  dgrval  20149  coef3  20153  coemulc  20175  dgrsub  20192  coecj  20198  dvply2  20205  dvnply  20207  quotval  20211  fta1  20227  plyexmo  20232  aacjcl  20246  taylfval  20277  dvtaylp  20288  abelth  20359  pilem2  20370  pilem3  20371  sinord  20438  recosf1o  20439  resinf1o  20440  tanord1  20441  eff1olem  20452  dvloglem  20541  dvlog  20544  dvlog2lem  20545  advlogexp  20548  logtayl  20553  logtayl2  20555  cxpcn3lem  20633  cxpcn3  20634  sqrcn  20636  loglesqr  20644  1cubr  20684  acosrecl  20745  rlimcnp2  20807  xrlimcnp  20809  efrlim  20810  jensen  20829  basellem4  20868  ppiprm  20936  chtprm  20938  prmorcht  20963  dvdsflip  20969  musum  20978  chpchtsum  21005  dchrinvcl  21039  dchrghm  21042  dchrinv  21047  dchrsum2  21054  dchrsum  21055  rplogsumlem2  21181  rpvmasumlem  21183  dchrisum0re  21209  dchrisum0lem2a  21213  dirith2  21224  pnt  21310  issubgoi  21900  opidon  21912  flddivrng  22005  rngosn3  22016  vcoprnelem  22059  nvvcop  22075  nvex  22092  phnv  22317  sheli  22718  cheli  22737  choc1  22831  shintcli  22833  chintcli  22835  shsleji  22874  pjini  23203  mayete3i  23232  mayete3iOLD  23233  dmadjop  23393  nlelshi  23565  cnlnadjeui  23582  cnlnssadj  23585  bdopadj  23587  pjimai  23681  stcl  23721  atelch  23849  disjin  24029  partfun  24089  iundisj2fi  24155  eliccioo  24179  xrsmulgzz  24202  xrge0mulgnn0  24212  xrge0nre  24215  xrge0tsmsd  24225  xrge0iifcnv  24321  xrge0iifcv  24322  xrge0iifiso  24323  xrge0iifhom  24325  qqhcn  24377  rnlogblem  24401  esumval  24443  gsumesum  24453  esumlub  24454  esumcst  24457  esumfsup  24462  issgon  24508  elrnsiga  24511  imambfm  24614  br2base  24621  sxbrsigalem0  24623  dya2iocucvr  24636  sxbrsigalem2  24638  sxbrsigalem5  24640  sxbrsiga  24642  sibfof  24656  sitmcl  24665  ballotlem2  24748  ballotlemfp1  24751  ballotlemfc0  24752  ballotlemfcc  24753  ballotlemfmpn  24754  ballotlemsup  24764  ballotlemfrceq  24788  lgamgulmlem2  24816  lgamucov2  24825  subfacp1lem5  24872  cvmsi  24954  dedekindle  25190  divcnvshft  25213  zprod  25265  risefaccllem  25331  fallfaccllem  25332  dfon2lem4  25415  wfrlem4  25543  wfrlem10  25549  frrlem4  25587  pprodss4v  25731  axlowdimlem5  25887  axlowdimlem6  25888  axlowdimlem7  25889  axlowdimlem15  25897  axlowdimlem16  25898  axlowdimlem17  25899  axlowdim  25902  axeuclidlem  25903  axcontlem2  25906  axcontlem7  25911  axcontlem8  25912  linedegen  26079  bpolydiflem  26102  bpoly4  26107  nnssi2  26207  nnssi3  26208  mblfinlem1  26245  cnambfre  26257  itg2addnc  26261  itg2gt0cn  26262  ftc1cnnc  26281  ftc2nc  26291  ivthALT  26340  neibastop2lem  26391  cover2  26417  opelopab3  26420  sstotbnd2  26485  heibor1lem  26520  heiborlem10  26531  exidcl  26553  elrfi  26750  elrfirn  26751  elrfirn2  26752  mrefg3  26764  diophin  26833  diophun  26834  eq0rabdioph  26837  eqrabdioph  26838  pellex  26900  rmxycomplete  26982  rmxypos  27014  ltrmynn0  27015  jm2.23  27069  aomclem2  27132  fglmod  27150  lsmfgcl  27151  lmhmfgima  27161  lmhmfgsplit  27163  frlmsslsp  27227  isnumbasabl  27250  islinds4  27284  lmimlbs  27285  lbslcic  27290  dgrsub2  27318  itgocn  27348  symgtrinv  27392  psgnpmtr  27412  psgnghm  27416  acsfn1p  27486  itgsin0pilem1  27722  itgsinexplem1  27726  itgsinexp  27727  stoweidlem34  27761  stoweidlem41  27768  stoweidlem51  27778  wallispilem2  27793  stirlinglem11  27811  elovmpt3rab1  28095  swrd0fv0  28215  cshwidxm1  28267  cshwidxm  28268  cshwidxn  28269  swrd0fvls  28286  cshwssizelem1a  28301  cshwssizelem3  28304  2wlkonot3v  28395  2spthonot3v  28396  onfrALTlem2  28694  onfrALTlem2VD  29063  bnj1533  29285  bnj1137  29426  bnj1286  29450  bnj1408  29467  bnj1417  29472  toycom  29832  osumcllem7N  30821  pexmidlem4N  30832  diaintclN  31918  dibintclN  32027  mapd1o  32508  hdmapevec  32698
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator