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

Theorem sseli 3466
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 3464 . 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 1870    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  sselii  3467  sseldi  3468  elun1  3639  elun2  3640  copsex2ga  4966  issref  5233  2elresin  5705  nfvres  5911  fvco4i  5959  mptrcl  5971  fvmptss  5974  fvmptex  5976  fvmptnf  5983  elfvmptrab1  5986  fvopab4ndm  5988  fvimacnvi  6011  elpreima  6017  iinpreima  6025  ofrfval  6553  ofval  6554  off  6560  nnon  6712  finds  6733  finds2  6735  offres  6802  eqopi  6841  op1steq  6849  dfoprab4  6864  bropopvvv  6887  curry1val  6900  curry2val  6904  reldmtpos  6989  wfrlem4  7047  wfrlem10  7053  smores3  7080  smores2  7081  frsuc  7162  nnfi  7771  unifpw  7883  f1opwfi  7884  fival  7932  fi0  7940  dffi2  7943  elfiun  7950  cantnfp1lem1  8182  cantnfp1lem3  8184  epfrs  8214  r1fin  8243  r1tr  8246  r1ordg  8248  r1ord3g  8249  r1val1  8256  tz9.12lem3  8259  tcrank  8354  cplem1  8359  hta  8367  tskwe  8383  cardprclem  8412  r0weon  8442  fodomfi2  8489  alephfplem3  8535  dfac12r  8574  ackbij1lem6  8653  ackbij1lem9  8656  ackbij1lem10  8657  ackbij1lem11  8658  ackbij1lem16  8663  ackbij1lem18  8665  ackbij2  8671  fin23lem24  8750  fin23lem26  8753  fin23lem28  8768  fin23lem30  8770  fin23lem31  8771  isfin1-3  8814  fin1a2lem6  8833  hsmexlem4  8857  hsmexlem5  8858  hsmexlem6  8859  axdc2lem  8876  axdc3lem2  8879  axcclem  8885  ac6num  8907  brdom5  8955  brdom4  8956  canthp1lem2  9077  r1tskina  9206  gruina  9242  grur1a  9243  pinn  9302  0nnq  9348  elpqn  9349  recn  9628  rexr  9685  dedekindle  9797  ltord1  10139  leord1  10140  eqord1  10141  nnre  10616  nncn  10617  nnind  10627  nnnn0  10876  nn0re  10878  nn0cn  10879  nnz  10959  nn0z  10960  nnq  11277  qcn  11278  rpre  11308  difreicc  11762  iccshftri  11765  iccshftli  11767  iccdili  11769  icccntri  11771  fzval2  11785  fzelp1  11846  4fvwrd4  11907  elfzo1  11962  ico01fl0  12050  expcllem  12280  expcl2lem  12281  m1expcl2  12291  bcm1k  12497  bcpasc  12503  hashbclem  12610  swrd0fv0  12781  swrd0fvlsw  12784  sqrlem5  13289  cau3lem  13396  caubnd  13400  climconst2  13590  rlimres  13600  lo1res  13601  lo1resb  13606  rlimresb  13607  o1resb  13608  o1of2  13654  o1rlimmul  13660  caurcvg  13720  caurcvgOLD  13721  caucvg  13723  ackbijnn  13864  binomlem  13865  incexclem  13872  divcnvshft  13891  zprod  13969  fprodge1  14027  risefaccllem  14044  fallfaccllem  14045  bpolydiflem  14085  bpoly4  14090  divalglem8  14356  sadadd  14415  smueqlem  14438  smumul  14441  isprm3  14595  phimullem  14687  prmdiveq  14694  unbenlem  14806  prmreclem2  14815  prmrec  14820  vdwnnlem1  14899  vdwnnlem3  14901  ramtcl2  14920  ramtcl2OLD  14921  prmgaplem4  14978  cshwshashlem1  15020  isstruct2  15084  structcnvcnv  15086  fvsetsid  15102  strlemor1  15170  imasdsval2  15364  xpsfrnel2  15413  mreunirn  15449  mrcfval  15456  mrisval  15478  isacs2  15501  acsfn  15507  homarcl  15865  arwval  15880  coafval  15901  coapm  15908  isdrs2  16126  isacs3lem  16354  psssdm2  16403  tsrss  16411  submnd0  16508  nmzsubg  16800  nmznsg  16803  resscntz  16927  cntzmhm  16934  symgtrinv  17055  pmtrdifellem4  17062  psgnpmtr  17093  efginvrel2  17303  efginvrel1  17304  efgsp1  17313  efgsres  17314  efgsfo  17315  frgpinv  17340  frgpupf  17349  frgpup1  17351  subcmn  17403  torsubg  17418  dprd2dlem1  17600  dpjidcl  17617  ablfaclem3  17646  subrgpropd  17968  lssacs  18116  sralmod  18336  psrbaglefi  18522  mplsubglem  18584  ressmpladd  18607  ressmplmul  18608  ressmplvsca  18609  mplmonmul  18614  mplind  18651  ply1bascl  18722  cnsubdrglem  18945  rege0subm  18950  rge0srg  18963  zringunit  18984  znrrg  19058  psgnghm  19070  zrhpsgnevpm  19081  evpmodpmf1o  19086  pmtrodpm  19087  frlmsslsp  19276  islinds4  19315  lmimlbs  19316  lbslcic  19321  mdetralt  19555  mdetunilem7  19565  chfacfpmmulgsum2  19811  basdif0  19890  tgval2  19893  mreclatdemoBAD  20034  ordtbas  20130  ordtrest  20140  ordtrestixx  20160  fincmp  20330  cmpfi  20345  bwth  20347  iuncon  20365  1stcrest  20390  hauslly  20429  kgentop  20479  ptbasin  20514  ptcnplem  20558  txkgen  20589  infil  20800  filunirn  20819  uzrest  20834  elflim  20908  hauspwpwf1  20924  flffval  20926  fclsval  20945  isfcls  20946  fcfval  20970  alexsubALTlem3  20986  alexsubALTlem4  20987  ustn0  21157  fmucndlem  21228  xmetunirn  21274  blbas  21367  blres  21368  mopnval  21375  setsmstopn  21415  tmsval  21418  tngtopn  21580  qtopbaslem  21681  xrtgioo  21726  reperflem  21738  icccmplem1  21742  reconnlem2  21747  xrge0tsms  21754  icopnfhmeo  21858  icccvx  21865  bndth  21873  reparphti  21912  pcofval  21925  pcoval1  21928  pcoval2  21931  pcoass  21939  pcorevlem  21941  pcorev2  21943  pi1xfrcnv  21972  nmhmcn  22018  csscld  22104  cfilfval  22118  caufval  22129  cfilres  22150  bcthlem1  22176  ivthlem1  22274  ivthlem3  22276  ovolicc2lem3  22341  ovolicc2lem4  22342  ioombl1lem4  22382  vitalilem1  22434  mbflimsup  22491  mbflimsupOLD  22492  i1fima2  22505  i1fd  22507  i1f0  22513  i1f1  22516  itg1addlem4  22525  itg1addlem5  22526  itg2cnlem2  22588  iblmbf  22593  ellimc2  22700  limcres  22709  limcun  22718  dvbsss  22725  perfdvf  22726  dvres2lem  22733  dvaddbr  22760  rolle  22810  cmvth  22811  dvlip  22813  dvlipcn  22814  dvle  22827  lhop1lem  22833  dvfsumle  22841  dvfsumge  22842  dvfsumabs  22843  dvfsumlem2  22847  ftc2  22864  itgparts  22867  itgsubstlem  22868  itgsubst  22869  deg1mul3  22932  coeval  23036  coeeu  23038  dgrval  23041  coef3  23045  coemulc  23068  dgrsub  23085  coecj  23091  dvply2  23098  dvnply  23100  quotval  23104  fta1  23120  plyexmo  23125  aacjcl  23139  taylfval  23170  dvtaylp  23181  abelth  23252  pilem2  23263  pilem2OLD  23264  pilem3  23265  pilem3OLD  23266  sinord  23339  recosf1o  23340  resinf1o  23341  tanord1  23342  eff1olem  23353  dvloglem  23449  dvlog  23452  dvlog2lem  23453  advlogexp  23456  logtayl  23461  logtayl2  23463  dvcncxp1  23539  dvcnsqrt  23540  cxpcn3lem  23543  cxpcn3  23544  sqrtcn  23546  loglesqrt  23554  1cubr  23624  acosrecl  23685  rlimcnp2  23748  xrlimcnp  23750  efrlim  23751  jensen  23770  lgamgulmlem2  23811  lgamucov2  23820  basellem4  23864  ppiprm  23932  chtprm  23934  prmorcht  23959  dvdsflip  23965  musum  23974  chpchtsum  24001  dchrinvcl  24035  dchrghm  24038  dchrinv  24043  dchrsum2  24050  dchrsum  24051  rplogsumlem2  24177  rpvmasumlem  24179  dchrisum0re  24205  dchrisum0lem2a  24209  dirith2  24220  pnt  24306  tglng  24442  axlowdimlem6  24814  axlowdimlem16  24824  axlowdimlem17  24825  axlowdim  24828  axeuclidlem  24829  axcontlem2  24832  axcontlem7  24837  axcontlem8  24838  clwwlknprop  25336  clwwisshclww  25371  2wlkonot3v  25439  2spthonot3v  25440  issubgoi  25874  opidonOLD  25886  flddivrng  25979  rngosn3  25990  vcoprnelem  26033  nvvcop  26049  nvex  26066  phnv  26291  sheli  26693  cheli  26711  choc1  26806  shintcli  26808  chintcli  26810  shsleji  26849  pjini  27178  mayete3i  27207  dmadjop  27367  nlelshi  27539  cnlnadjeui  27556  cnlnssadj  27559  bdopadj  27561  pjimai  27655  stcl  27695  atelch  27823  disjin  28026  disjin2  28027  fcnvgreu  28106  partfun  28109  f1od2  28143  fcobijfs  28145  xrge0infss  28172  iundisj2fi  28200  nnindf  28211  eliccioo  28229  xrge0mulgnn0  28279  xrge0nre  28282  xrge0omnd  28303  gsummptres  28377  prsdm  28550  prsrn  28551  ordtrestNEW  28557  xrge0iifcnv  28569  xrge0iifcv  28570  xrge0iifiso  28571  xrge0iifhom  28573  qqhcn  28625  esumval  28697  gsumesum  28710  esumlub  28711  esumcst  28714  esumfsup  28721  esumcvgre  28742  issgon  28775  elrnsiga  28778  imambfm  28914  br2base  28921  sxbrsigalem0  28923  dya2iocucvr  28936  sxbrsigalem2  28938  sxbrsigalem5  28940  sxbrsiga  28942  omssubadd  28952  oddpwdc  29004  eulerpartlemelr  29007  eulerpartgbij  29022  eulerpartlemgvv  29026  eulerpartlemgh  29028  eulerpartlemgs2  29030  eulerpartlemn  29031  sseqf  29042  ballotlem2  29138  ballotlemfp1  29141  ballotlemfc0  29142  ballotlemfcc  29143  ballotlemfmpn  29144  ballotlemsup  29154  ballotlemfrceq  29178  signswch  29229  bnj1533  29442  bnj1137  29583  bnj1286  29607  bnj1408  29624  bnj1417  29629  subfacp1lem5  29686  cvmsi  29767  mpst123  29957  mpstrcl  29958  msrrcl  29960  elmsta  29965  msubvrs  29977  elmpps  29990  elmthm  29993  bcprod  30152  dfon2lem4  30210  frrlem4  30295  pprodss4v  30427  ivthALT  30767  neibastop2lem  30792  nnssi2  30891  nnssi3  30892  bj-sngltagi  31316  bj-elid  31375  bj-elid2  31376  bj-cmnssmndel  31428  bj-ablssgrpel  31430  bj-ablsscmnel  31432  bj-vecssmodel  31435  bj-rrvecssvecel  31442  bj-rrvecsscmnel  31444  taupilemrplb  31457  icorempt2  31479  sin2h  31629  cos2h  31630  tan2h  31631  poimirlem14  31648  poimirlem26  31660  poimirlem27  31661  poimirlem31  31665  poimirlem32  31666  heicant  31669  mblfinlem1  31671  cnambfre  31683  dvtan  31686  itg2addnc  31690  itg2gt0cn  31691  ftc1cnnc  31710  ftc2nc  31720  dvasin  31722  dvacos  31723  cover2  31734  sstotbnd2  31800  heibor1lem  31835  heiborlem10  31846  exidcl  31868  toycom  32238  osumcllem7N  33226  pexmidlem4N  33237  diaintclN  34325  dibintclN  34434  mapd1o  34915  hdmapevec  35105  elrfi  35235  elrfirn  35236  elrfirn2  35237  mrefg3  35249  diophin  35314  diophun  35315  eq0rabdioph  35318  eqrabdioph  35319  pellex  35379  rmxycomplete  35461  jm2.23  35547  aomclem2  35609  fglmod  35627  lsmfgcl  35628  lmhmfgima  35638  lmhmfgsplit  35640  isnumbasabl  35661  dgrsub2  35690  itgocn  35719  acsfn1p  35754  areaquad  35790  fiinfi  35866  corcltrcl  35960  radcnvrat  36290  uzmptshftfval  36322  binomcxplemdvsum  36331  binomcxplemnotnn0  36332  onfrALTlem2  36539  onfrALTlem2VD  36916  uzwo4  37023  disjinfi  37081  eliccxr  37187  eliccelioc  37197  fsumiunss  37219  limcdm0  37260  sumnnodd  37272  cncfshift  37313  cncfperiod  37318  icccncfext  37327  dvnprodlem1  37380  dvnprodlem2  37381  itgsin0pilem1  37385  itgsinexplem1  37389  itgsinexp  37390  ditgeqiooicc  37396  itgsubsticclem  37411  itgioocnicc  37413  itgsbtaddcnst  37418  stoweidlem34  37454  stoweidlem41  37461  stoweidlem51  37471  wallispilem2  37487  stirlinglem11  37505  dirkercncflem2  37525  fourierdlem5  37533  fourierdlem9  37537  fourierdlem17  37545  fourierdlem18  37546  fourierdlem20  37548  fourierdlem39  37567  fourierdlem48  37576  fourierdlem49  37577  fourierdlem62  37590  fourierdlem66  37594  fourierdlem68  37596  fourierdlem72  37600  fourierdlem73  37601  fourierdlem81  37609  fourierdlem83  37611  fourierdlem85  37613  fourierdlem87  37615  fourierdlem88  37616  fourierdlem92  37620  fourierdlem95  37623  fourierdlem103  37631  fourierdlem104  37632  fourierdlem112  37640  sqwvfoura  37650  sqwvfourb  37651  fouriersw  37653  etransclem24  37680  etransclem35  37691  etransclem37  37693  gsumge0cl  37737  sge0tsms  37746  sge0resplit  37772  sge0split  37775  caratheodorylem1  37846  bgoldbtbndlem2  38281  bgoldbtbndlem3  38282  bgoldbtbnd  38284  pfxfv0  38321  pfxfvlsw  38324  fldhmsubc  38834  fldhmsubcALTV  38853
  Copyright terms: Public domain W3C validator