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

Theorem sseli 3398
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 3396 . 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 1872    C_ wss 3374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-in 3381  df-ss 3388
This theorem is referenced by:  sselii  3399  sseldi  3400  elun1  3571  elun2  3572  copsex2ga  4903  issref  5170  2elresin  5643  nfvres  5850  fvco4i  5898  mptrcl  5910  fvmptss  5913  fvmptex  5915  fvmptnf  5922  elfvmptrab1  5925  fvopab4ndm  5927  fvimacnvi  5950  elpreima  5956  iinpreima  5964  ofrfval  6492  ofval  6493  off  6499  nnon  6651  finds  6672  finds2  6674  offres  6741  eqopi  6780  op1steq  6788  dfoprab4  6803  bropopvvv  6826  curry1val  6839  curry2val  6843  reldmtpos  6931  wfrlem4  6989  wfrlem10  6995  smores3  7022  smores2  7023  frsuc  7104  nnfi  7713  unifpw  7825  f1opwfi  7826  fival  7874  fi0  7882  dffi2  7885  elfiun  7892  cantnfp1lem1  8130  cantnfp1lem3  8132  epfrs  8162  r1fin  8191  r1tr  8194  r1ordg  8196  r1ord3g  8197  r1val1  8204  tz9.12lem3  8207  tcrank  8302  cplem1  8307  hta  8315  tskwe  8331  cardprclem  8360  r0weon  8390  fodomfi2  8437  alephfplem3  8483  dfac12r  8522  ackbij1lem6  8601  ackbij1lem9  8604  ackbij1lem10  8605  ackbij1lem11  8606  ackbij1lem16  8611  ackbij1lem18  8613  ackbij2  8619  fin23lem24  8698  fin23lem26  8701  fin23lem28  8716  fin23lem30  8718  fin23lem31  8719  isfin1-3  8762  fin1a2lem6  8781  hsmexlem4  8805  hsmexlem5  8806  hsmexlem6  8807  axdc2lem  8824  axdc3lem2  8827  axcclem  8833  ac6num  8855  brdom5  8903  brdom4  8904  canthp1lem2  9024  r1tskina  9153  gruina  9189  grur1a  9190  pinn  9249  0nnq  9295  elpqn  9296  recn  9575  rexr  9632  dedekindle  9744  ltord1  10086  leord1  10087  eqord1  10088  nnre  10562  nncn  10563  nnind  10573  nnnn0  10822  nn0re  10824  nn0cn  10825  nnz  10905  nn0z  10906  nnq  11223  qcn  11224  rpre  11254  difreicc  11710  iccshftri  11713  iccshftli  11715  iccdili  11717  icccntri  11719  fzval2  11733  fzelp1  11794  4fvwrd4  11855  elfzo1  11910  ico01fl0  11998  expcllem  12228  expcl2lem  12229  m1expcl2  12239  bcm1k  12445  bcpasc  12451  hashbclem  12558  swrd0fv0  12737  swrd0fvlsw  12740  sqrlem5  13249  cau3lem  13356  caubnd  13360  climconst2  13550  rlimres  13560  lo1res  13561  lo1resb  13566  rlimresb  13567  o1resb  13568  o1of2  13614  o1rlimmul  13620  caurcvg  13680  caurcvgOLD  13681  caucvg  13683  ackbijnn  13824  binomlem  13825  incexclem  13832  divcnvshft  13851  zprod  13929  fprodge1  13987  risefaccllem  14004  fallfaccllem  14005  bpolydiflem  14045  bpoly4  14050  divalglem8  14318  sadadd  14379  smueqlem  14402  smumul  14405  isprm3  14571  phimullem  14665  prmdiveq  14672  unbenlem  14790  prmreclem2  14799  prmrec  14804  vdwnnlem1  14883  vdwnnlem3  14885  ramtcl2  14904  ramtcl2OLD  14905  prmgaplem4  14962  cshwshashlem1  15004  isstruct2  15068  structcnvcnv  15070  fvsetsid  15086  strlemor1  15155  imasdsval2  15355  imasdsval2OLD  15367  xpsfrnel2  15409  mreunirn  15445  mrcfval  15452  mrisval  15474  isacs2  15497  acsfn  15503  homarcl  15861  arwval  15876  coafval  15897  coapm  15904  isdrs2  16122  isacs3lem  16350  psssdm2  16399  tsrss  16407  submnd0  16504  nmzsubg  16796  nmznsg  16799  resscntz  16923  cntzmhm  16930  symgtrinv  17051  pmtrdifellem4  17058  psgnpmtr  17089  efginvrel2  17315  efginvrel1  17316  efgsp1  17325  efgsres  17326  efgsfo  17327  frgpinv  17352  frgpupf  17361  frgpup1  17363  subcmn  17415  torsubg  17430  dprd2dlem1  17612  dpjidcl  17629  ablfaclem3  17658  subrgpropd  17980  lssacs  18128  sralmod  18348  psrbaglefi  18534  mplsubglem  18596  ressmpladd  18619  ressmplmul  18620  ressmplvsca  18621  mplmonmul  18626  mplind  18663  ply1bascl  18734  cnsubdrglem  18957  rege0subm  18962  rge0srg  18975  zringunit  18999  znrrg  19073  psgnghm  19085  zrhpsgnevpm  19096  evpmodpmf1o  19101  pmtrodpm  19102  frlmsslsp  19291  islinds4  19330  lmimlbs  19331  lbslcic  19336  mdetralt  19570  mdetunilem7  19580  chfacfpmmulgsum2  19826  basdif0  19905  tgval2  19908  mreclatdemoBAD  20049  ordtbas  20145  ordtrest  20155  ordtrestixx  20175  fincmp  20345  cmpfi  20360  bwth  20362  iuncon  20380  1stcrest  20405  hauslly  20444  kgentop  20494  ptbasin  20529  ptcnplem  20573  txkgen  20604  infil  20815  filunirn  20834  uzrest  20849  elflim  20923  hauspwpwf1  20939  flffval  20941  fclsval  20960  isfcls  20961  fcfval  20985  alexsubALTlem3  21001  alexsubALTlem4  21002  ustn0  21172  fmucndlem  21243  xmetunirn  21289  blbas  21382  blres  21383  mopnval  21390  setsmstopn  21430  tmsval  21433  tngtopn  21595  qtopbaslem  21716  xrtgioo  21761  reperflem  21773  icccmplem1  21777  reconnlem2  21782  xrge0tsms  21789  icopnfhmeo  21908  icccvx  21915  bndth  21923  reparphti  21965  pcofval  21978  pcoval1  21981  pcoval2  21984  pcoass  21992  pcorevlem  21994  pcorev2  21996  pi1xfrcnv  22025  nmhmcn  22071  csscld  22157  cfilfval  22171  caufval  22182  cfilres  22203  bcthlem1  22229  ivthlem1  22339  ivthlem3  22341  ovolicc2lem3  22409  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  ioombl1lem4  22451  vitalilem1  22503  mbflimsup  22560  mbflimsupOLD  22561  i1fima2  22574  i1fd  22576  i1f0  22582  i1f1  22585  itg1addlem4  22594  itg1addlem5  22595  itg2cnlem2  22657  iblmbf  22662  ellimc2  22769  limcres  22778  limcun  22787  dvbsss  22794  perfdvf  22795  dvres2lem  22802  dvaddbr  22829  rolle  22879  cmvth  22880  dvlip  22882  dvlipcn  22883  dvle  22896  lhop1lem  22902  dvfsumle  22910  dvfsumge  22911  dvfsumabs  22912  dvfsumlem2  22916  ftc2  22933  itgparts  22936  itgsubstlem  22937  itgsubst  22938  deg1mul3  23001  coeval  23114  coeeu  23116  dgrval  23119  coef3  23123  coemulc  23146  dgrsub  23163  coecj  23169  dvply2  23176  dvnply  23178  quotval  23182  fta1  23198  plyexmo  23203  aacjcl  23220  taylfval  23251  dvtaylp  23262  abelth  23333  pilem2  23344  pilem2OLD  23345  pilem3  23346  pilem3OLD  23347  sinord  23420  recosf1o  23421  resinf1o  23422  tanord1  23423  eff1olem  23434  dvloglem  23530  dvlog  23533  dvlog2lem  23534  advlogexp  23537  logtayl  23542  logtayl2  23544  dvcncxp1  23620  dvcnsqrt  23621  cxpcn3lem  23624  cxpcn3  23625  sqrtcn  23627  loglesqrt  23635  1cubr  23705  acosrecl  23766  rlimcnp2  23829  xrlimcnp  23831  efrlim  23832  jensen  23851  lgamgulmlem2  23892  lgamucov2  23901  basellem4  23947  ppiprm  24015  chtprm  24017  prmorcht  24042  dvdsflip  24048  musum  24057  chpchtsum  24084  dchrinvcl  24118  dchrghm  24121  dchrinv  24126  dchrsum2  24133  dchrsum  24134  rplogsumlem2  24260  rpvmasumlem  24262  dchrisum0re  24288  dchrisum0lem2a  24292  dirith2  24303  pnt  24389  tglng  24528  axlowdimlem6  24914  axlowdimlem16  24924  axlowdimlem17  24925  axlowdim  24928  axeuclidlem  24929  axcontlem2  24932  axcontlem7  24937  axcontlem8  24938  clwwlknprop  25437  clwwisshclww  25472  2wlkonot3v  25540  2spthonot3v  25541  issubgoi  25975  opidonOLD  25987  flddivrng  26080  rngosn3  26091  vcoprnelem  26134  nvvcop  26150  nvex  26167  phnv  26392  sheli  26804  cheli  26822  choc1  26917  shintcli  26919  chintcli  26921  shsleji  26960  pjini  27289  mayete3i  27318  dmadjop  27478  nlelshi  27650  cnlnadjeui  27667  cnlnssadj  27670  bdopadj  27672  pjimai  27766  stcl  27806  atelch  27934  disjin  28137  disjin2  28138  fcnvgreu  28216  partfun  28219  f1od2  28254  fcobijfs  28256  xrge0infss  28285  xrge0infssOLD  28286  iundisj2fi  28318  nnindf  28328  eliccioo  28346  xrge0mulgnn0  28397  xrge0nre  28399  xrge0omnd  28420  gsummptres  28494  prsdm  28667  prsrn  28668  ordtrestNEW  28674  xrge0iifcnv  28686  xrge0iifcv  28687  xrge0iifiso  28688  xrge0iifhom  28690  qqhcn  28742  esumval  28814  gsumesum  28827  esumlub  28828  esumcst  28831  esumfsup  28838  esumcvgre  28859  issgon  28892  elrnsiga  28895  imambfm  29031  br2base  29038  sxbrsigalem0  29040  dya2iocucvr  29053  sxbrsigalem2  29055  sxbrsigalem5  29057  sxbrsiga  29059  omssubadd  29075  omssubaddOLD  29079  sitmcl  29131  oddpwdc  29134  eulerpartlemelr  29137  eulerpartgbij  29152  eulerpartlemgvv  29156  eulerpartlemgh  29158  eulerpartlemgs2  29160  eulerpartlemn  29161  sseqf  29172  ballotlem2  29268  ballotlemfp1  29271  ballotlemfc0  29272  ballotlemfcc  29273  ballotlemfmpn  29274  ballotlemsup  29284  ballotlemfrceq  29308  ballotlemsupOLD  29322  ballotlemfrceqOLD  29346  signswch  29397  bnj1533  29610  bnj1137  29751  bnj1286  29775  bnj1408  29792  bnj1417  29797  subfacp1lem5  29854  cvmsi  29935  mpst123  30125  mpstrcl  30126  msrrcl  30128  elmsta  30133  msubvrs  30145  elmpps  30158  elmthm  30161  bcprod  30320  dfon2lem4  30378  frrlem4  30463  pprodss4v  30595  ivthALT  30935  neibastop2lem  30960  nnssi2  31059  nnssi3  31060  bj-sngltagi  31487  bj-elid  31546  bj-elid2  31547  bj-cmnssmndel  31599  bj-ablssgrpel  31601  bj-ablsscmnel  31603  bj-vecssmodel  31606  bj-rrvecssvecel  31613  bj-rrvecsscmnel  31615  taupilemrplb  31628  icorempt2  31661  elxp8  31681  sin2h  31842  cos2h  31843  tan2h  31844  poimirlem14  31861  poimirlem26  31873  poimirlem27  31874  poimirlem31  31878  poimirlem32  31879  mblfinlem1  31884  cnambfre  31896  dvtan  31899  itg2addnc  31903  itg2gt0cn  31904  ftc1cnnc  31923  ftc2nc  31933  dvasin  31935  dvacos  31936  cover2  31947  sstotbnd2  32013  heibor1lem  32048  heiborlem10  32059  exidcl  32081  toycom  32451  osumcllem7N  33439  pexmidlem4N  33450  diaintclN  34538  dibintclN  34647  mapd1o  35128  hdmapevec  35318  elrfi  35448  elrfirn  35449  elrfirn2  35450  mrefg3  35462  diophin  35527  diophun  35528  eq0rabdioph  35531  eqrabdioph  35532  pellex  35592  rmxycomplete  35678  jm2.23  35764  aomclem2  35826  fglmod  35844  lsmfgcl  35845  lmhmfgima  35855  lmhmfgsplit  35857  isnumbasabl  35878  dgrsub2  35907  itgocn  35943  acsfn1p  35978  areaquad  36014  elmapintrab  36095  corcltrcl  36244  radcnvrat  36576  uzmptshftfval  36608  binomcxplemdvsum  36617  binomcxplemnotnn0  36618  onfrALTlem2  36825  onfrALTlem2VD  37202  uzwo4  37308  disjinfi  37372  eliccxr  37504  eliccelioc  37514  elicores  37526  fsumiunss  37538  limcdm0  37581  sumnnodd  37593  cncfshift  37634  cncfperiod  37639  icccncfext  37648  dvnprodlem1  37704  dvnprodlem2  37705  itgsin0pilem1  37709  itgsinexplem1  37713  itgsinexp  37714  ditgeqiooicc  37720  itgsubsticclem  37735  itgioocnicc  37737  itgsbtaddcnst  37742  stoweidlem34  37778  stoweidlem41  37785  stoweidlem51  37795  wallispilem2  37811  stirlinglem11  37829  dirkercncflem2  37849  fourierdlem5  37857  fourierdlem9  37861  fourierdlem17  37869  fourierdlem18  37870  fourierdlem20  37872  fourierdlem39  37892  fourierdlem48  37901  fourierdlem49  37902  fourierdlem62  37915  fourierdlem66  37919  fourierdlem68  37921  fourierdlem72  37925  fourierdlem73  37926  fourierdlem81  37934  fourierdlem83  37936  fourierdlem85  37938  fourierdlem87  37940  fourierdlem88  37941  fourierdlem92  37945  fourierdlem95  37948  fourierdlem103  37956  fourierdlem104  37957  fourierdlem112  37965  sqwvfoura  37975  sqwvfourb  37976  fouriersw  37978  etransclem24  38006  etransclem35  38017  etransclem37  38019  gsumge0cl  38064  sge0tsms  38073  sge0resplit  38099  sge0split  38102  caratheodorylem1  38198  volicorescl  38222  hoidmv1lelem3  38262  bgoldbtbndlem2  38714  bgoldbtbndlem3  38715  bgoldbtbnd  38717  pfxfv0  38754  pfxfvlsw  38757  fldhmsubc  39677  fldhmsubcALTV  39696
  Copyright terms: Public domain W3C validator