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

Theorem sseli 3485
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 3483 . 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 1804    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  sselii  3486  sseldi  3487  elun1  3656  elun2  3657  copsex2ga  5104  issref  5370  2elresin  5682  nfvres  5886  fvco4i  5936  fvmptss  5949  fvmptex  5951  fvmptnf  5958  elfvmptrab1  5961  fvopab4ndm  5963  fvimacnvi  5986  elpreima  5992  iinpreima  6002  ofrfval  6533  ofval  6534  off  6539  nnon  6691  finds  6711  finds2  6713  offres  6780  eqopi  6819  op1steq  6827  dfoprab4  6842  bropopvvv  6865  curry1val  6878  curry2val  6882  reldmtpos  6965  smores3  7026  smores2  7027  frsuc  7104  nnfi  7712  unifpw  7825  f1opwfi  7826  fival  7874  fi0  7882  dffi2  7885  elfiun  7892  cantnfp1lem1  8100  cantnfp1lem3  8102  cantnfp1lem1OLD  8126  cantnfp1lem3OLD  8128  epfrs  8165  r1fin  8194  r1tr  8197  r1ordg  8199  r1ord3g  8200  r1val1  8207  tz9.12lem3  8210  tcrank  8305  cplem1  8310  hta  8318  tskwe  8334  cardprclem  8363  r0weon  8393  fodomfi2  8444  alephfplem3  8490  dfac12r  8529  ackbij1lem6  8608  ackbij1lem9  8611  ackbij1lem10  8612  ackbij1lem11  8613  ackbij1lem16  8618  ackbij1lem18  8620  ackbij2  8626  fin23lem24  8705  fin23lem26  8708  fin23lem28  8723  fin23lem30  8725  fin23lem31  8726  isfin1-3  8769  fin1a2lem6  8788  hsmexlem4  8812  hsmexlem5  8813  hsmexlem6  8814  axdc2lem  8831  axdc3lem2  8834  axcclem  8840  ac6num  8862  brdom5  8910  brdom4  8911  canthp1lem2  9034  r1tskina  9163  gruina  9199  grur1a  9200  pinn  9259  0nnq  9305  elpqn  9306  recn  9585  rexr  9642  dedekindle  9748  ltord1  10086  leord1  10087  eqord1  10088  nnre  10550  nncn  10551  nnind  10561  nnnn0  10809  nn0re  10811  nn0cn  10812  nnz  10893  nn0z  10894  nnq  11206  qcn  11207  rpre  11237  difreicc  11663  iccshftri  11666  iccshftli  11668  iccdili  11670  icccntri  11672  fzval2  11686  fzelp1  11743  4fvwrd4  11804  elfzo1  11853  expcllem  12159  expcl2lem  12160  m1expcl2  12170  bcm1k  12375  bcpasc  12381  hashbclem  12483  swrd0fv0  12649  swrd0fvlsw  12652  sqrlem5  13062  cau3lem  13169  caubnd  13173  climconst2  13353  rlimres  13363  lo1res  13364  lo1resb  13369  rlimresb  13370  o1resb  13371  o1of2  13417  o1rlimmul  13423  caurcvg  13481  caucvg  13483  ackbijnn  13622  binomlem  13623  incexclem  13630  zprod  13726  divalglem8  14040  sadadd  14099  smueqlem  14122  smumul  14125  isprm3  14208  phimullem  14291  prmdiveq  14298  unbenlem  14408  prmreclem2  14417  prmrec  14422  vdwnnlem1  14495  vdwnnlem3  14497  ramtcl2  14511  cshwshashlem1  14562  isstruct2  14623  structcnvcnv  14625  fvsetsid  14639  strlemor1  14706  imasdsval2  14895  xpsfrnel2  14944  mreunirn  14980  mrcfval  14987  mrisval  15009  isacs2  15032  acsfn  15038  homarcl  15334  arwval  15349  coafval  15370  coapm  15377  isdrs2  15547  isacs3lem  15775  psssdm2  15824  tsrss  15832  submnd0  15929  nmzsubg  16221  nmznsg  16224  resscntz  16348  cntzmhm  16355  symgtrinv  16476  pmtrdifellem4  16483  psgnpmtr  16514  efginvrel2  16724  efginvrel1  16725  efgsp1  16734  efgsres  16735  efgsfo  16736  frgpinv  16761  frgpupf  16770  frgpup1  16772  subcmn  16824  torsubg  16839  dprd2dlem1  17069  dpjidcl  17086  dpjidclOLD  17093  ablfaclem3  17117  subrgpropd  17442  lssacs  17592  sralmod  17812  psrbaglefi  18002  psrbaglefiOLD  18003  mplsubglem  18072  mplsubglemOLD  18074  ressmpladd  18098  ressmplmul  18099  ressmplvsca  18100  mplmonmul  18105  mplind  18146  ply1bascl  18221  cnsubdrglem  18448  rege0subm  18453  rge0srg  18466  zringunit  18498  zrngunit  18499  znrrg  18582  psgnghm  18594  zrhpsgnevpm  18605  evpmodpmf1o  18610  pmtrodpm  18611  frlmsslsp  18807  frlmsslspOLD  18808  islinds4  18848  lmimlbs  18849  lbslcic  18854  mdetralt  19088  mdetunilem7  19098  chfacfpmmulgsum2  19344  basdif0  19432  tgval2  19435  mreclatdemoBAD  19575  ordtbas  19671  ordtrest  19681  ordtrestixx  19701  fincmp  19871  cmpfi  19886  bwth  19888  iuncon  19907  1stcrest  19932  hauslly  19971  kgentop  20021  ptbasin  20056  ptcnplem  20100  txkgen  20131  infil  20342  filunirn  20361  uzrest  20376  elflim  20450  hauspwpwf1  20466  flffval  20468  fclsval  20487  isfcls  20488  fcfval  20512  alexsubALTlem3  20527  alexsubALTlem4  20528  ustn0  20701  fmucndlem  20772  xmetunirn  20818  blbas  20911  blres  20912  mopnval  20919  setsmstopn  20959  tmsval  20962  tngtopn  21142  qtopbaslem  21243  xrtgioo  21289  reperflem  21301  icccmplem1  21305  reconnlem2  21310  xrge0tsms  21317  icopnfhmeo  21421  icccvx  21428  bndth  21436  reparphti  21475  pcofval  21488  pcoval1  21491  pcoval2  21494  pcoass  21502  pcorevlem  21504  pcorev2  21506  pi1xfrcnv  21535  nmhmcn  21581  csscld  21667  cfilfval  21681  caufval  21692  cfilres  21713  bcthlem1  21741  ivthlem1  21841  ivthlem3  21843  ovolicc2lem3  21908  ovolicc2lem4  21909  ioombl1lem4  21949  vitalilem1  21995  mbflimsup  22051  i1fima2  22064  i1fd  22066  i1f0  22072  i1f1  22075  itg1addlem4  22084  itg1addlem5  22085  itg2cnlem2  22147  iblmbf  22152  ellimc2  22259  limcres  22268  limcun  22277  dvbsss  22284  perfdvf  22285  dvres2lem  22292  dvaddbr  22319  rolle  22369  cmvth  22370  dvlip  22372  dvlipcn  22373  dvle  22386  lhop1lem  22392  dvfsumle  22400  dvfsumge  22401  dvfsumabs  22402  dvfsumlem2  22406  ftc2  22423  itgparts  22426  itgsubstlem  22427  itgsubst  22428  deg1mul3  22494  coeval  22598  coeeu  22600  dgrval  22603  coef3  22607  coemulc  22630  dgrsub  22647  coecj  22653  dvply2  22660  dvnply  22662  quotval  22666  fta1  22682  plyexmo  22687  aacjcl  22701  taylfval  22732  dvtaylp  22743  abelth  22814  pilem2  22825  pilem3  22826  sinord  22899  recosf1o  22900  resinf1o  22901  tanord1  22902  eff1olem  22913  dvloglem  23007  dvlog  23010  dvlog2lem  23011  advlogexp  23014  logtayl  23019  logtayl2  23021  cxpcn3lem  23099  cxpcn3  23100  sqrtcn  23102  loglesqrt  23110  1cubr  23151  acosrecl  23212  rlimcnp2  23274  xrlimcnp  23276  efrlim  23277  jensen  23296  basellem4  23335  ppiprm  23403  chtprm  23405  prmorcht  23430  dvdsflip  23436  musum  23445  chpchtsum  23472  dchrinvcl  23506  dchrghm  23509  dchrinv  23514  dchrsum2  23521  dchrsum  23522  rplogsumlem2  23648  rpvmasumlem  23650  dchrisum0re  23676  dchrisum0lem2a  23680  dirith2  23691  pnt  23777  tglng  23911  axlowdimlem6  24228  axlowdimlem16  24238  axlowdimlem17  24239  axlowdim  24242  axeuclidlem  24243  axcontlem2  24246  axcontlem7  24251  axcontlem8  24252  clwwlknprop  24750  clwwisshclww  24785  2wlkonot3v  24853  2spthonot3v  24854  issubgoi  25290  opidonOLD  25302  flddivrng  25395  rngosn3  25406  vcoprnelem  25449  nvvcop  25465  nvex  25482  phnv  25707  sheli  26109  cheli  26128  choc1  26223  shintcli  26225  chintcli  26227  shsleji  26266  pjini  26595  mayete3i  26624  mayete3iOLD  26625  dmadjop  26785  nlelshi  26957  cnlnadjeui  26974  cnlnssadj  26977  bdopadj  26979  pjimai  27073  stcl  27113  atelch  27241  disjin  27424  fcnvgreu  27492  partfun  27494  f1od2  27525  fcobijfs  27527  xrge0infss  27558  iundisj2fi  27580  nnindf  27588  eliccioo  27605  xrge0mulgnn0  27655  xrge0nre  27658  xrge0omnd  27679  xrge0tsmsd  27753  prsdm  27874  prsrn  27875  ordtrestNEW  27881  xrge0iifcnv  27893  xrge0iifcv  27894  xrge0iifiso  27895  xrge0iifhom  27897  qqhcn  27950  esumval  28035  gsumesum  28045  esumlub  28046  esumcst  28049  esumfsup  28054  issgon  28101  elrnsiga  28104  imambfm  28211  br2base  28218  sxbrsigalem0  28220  dya2iocucvr  28233  sxbrsigalem2  28235  sxbrsigalem5  28237  sxbrsiga  28239  oddpwdc  28271  eulerpartlemelr  28274  eulerpartgbij  28289  eulerpartlemgvv  28293  eulerpartlemgh  28295  eulerpartlemgs2  28297  eulerpartlemn  28298  sseqf  28309  ballotlem2  28405  ballotlemfp1  28408  ballotlemfc0  28409  ballotlemfcc  28410  ballotlemfmpn  28411  ballotlemsup  28421  ballotlemfrceq  28445  signswch  28496  lgamgulmlem2  28550  lgamucov2  28559  subfacp1lem5  28606  cvmsi  28688  mpst123  28878  mpstrcl  28879  msrrcl  28881  elmsta  28886  msubvrs  28898  elmpps  28911  elmthm  28914  divcnvshft  29095  risefaccllem  29111  fallfaccllem  29112  dfon2lem4  29194  wfrlem4  29322  wfrlem10  29328  frrlem4  29366  pprodss4v  29510  bpolydiflem  29792  bpoly4  29797  nnssi2  29896  nnssi3  29897  sin2h  30021  cos2h  30022  tan2h  30023  heicant  30025  mblfinlem1  30027  cnambfre  30039  dvtan  30041  itg2addnc  30045  itg2gt0cn  30046  ftc1cnnc  30065  ftc2nc  30075  dvcncxp1  30076  dvcnsqrt  30077  dvasin  30079  dvacos  30080  ivthALT  30129  neibastop2lem  30154  cover2  30180  sstotbnd2  30246  heibor1lem  30281  heiborlem10  30292  exidcl  30314  elrfi  30602  elrfirn  30603  elrfirn2  30604  mrefg3  30616  diophin  30682  diophun  30683  eq0rabdioph  30686  eqrabdioph  30687  pellex  30747  rmxycomplete  30829  jm2.23  30914  aomclem2  30977  fglmod  30995  lsmfgcl  30996  lmhmfgima  31006  lmhmfgsplit  31008  isnumbasabl  31031  dgrsub2  31060  itgocn  31089  acsfn1p  31124  areaquad  31160  radcnvrat  31171  eliccxr  31504  eliccelioc  31515  fprodge1  31552  limcdm0  31578  sumnnodd  31590  cncfshift  31630  cncfperiod  31635  icccncfext  31644  dvnprodlem1  31697  dvnprodlem2  31698  itgsin0pilem1  31702  itgsinexplem1  31706  itgsinexp  31707  ditgeqiooicc  31713  itgsubsticclem  31728  itgioocnicc  31730  itgsbtaddcnst  31735  stoweidlem34  31770  stoweidlem41  31777  stoweidlem51  31787  wallispilem2  31802  stirlinglem11  31820  dirkercncflem2  31840  fourierdlem5  31848  fourierdlem9  31852  fourierdlem17  31860  fourierdlem18  31861  fourierdlem20  31863  fourierdlem39  31882  fourierdlem48  31891  fourierdlem49  31892  fourierdlem62  31905  fourierdlem66  31909  fourierdlem68  31911  fourierdlem72  31915  fourierdlem73  31916  fourierdlem81  31924  fourierdlem83  31926  fourierdlem85  31928  fourierdlem87  31930  fourierdlem88  31931  fourierdlem92  31935  fourierdlem95  31938  fourierdlem103  31946  fourierdlem104  31947  fourierdlem112  31955  sqwvfoura  31965  sqwvfourb  31966  fouriersw  31968  etransclem3  31974  etransclem24  31995  etransclem31  32002  etransclem35  32006  etransclem44  32015  fldhmsubc  32760  fldhmsubcOLD  32779  onfrALTlem2  33186  onfrALTlem2VD  33557  bnj1533  33778  bnj1137  33919  bnj1286  33943  bnj1408  33960  bnj1417  33965  bj-sngltagi  34423  bj-elid  34474  bj-elid2  34475  bj-flbi3  34483  bj-cmnssmndel  34528  bj-ablssgrpel  34530  bj-ablsscmnel  34532  bj-vecssmodel  34535  bj-rrvecssvecel  34542  bj-rrvecsscmnel  34544  toycom  34573  osumcllem7N  35561  pexmidlem4N  35572  diaintclN  36660  dibintclN  36769  mapd1o  37250  hdmapevec  37440  taupilemrplb  37570  fiinfi  37596
  Copyright terms: Public domain W3C validator