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

Theorem sseli 3450
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 3448 . 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 1758    C_ wss 3426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440
This theorem is referenced by:  sselii  3451  sseldi  3452  elun1  3621  elun2  3622  copsex2ga  5049  issref  5309  2elresin  5620  nfvres  5819  fvco4i  5868  fvmptss  5881  fvmptex  5883  fvmptnf  5890  fvopab4ndm  5893  fvimacnvi  5916  elpreima  5922  iinpreima  5932  ofrfval  6428  ofval  6429  off  6434  nnon  6582  finds  6602  finds2  6604  offres  6672  eqopi  6710  op1steq  6718  dfoprab4  6731  bropopvvv  6753  curry1val  6765  curry2val  6769  reldmtpos  6853  smores3  6914  smores2  6915  frsuc  6992  nnfi  7604  unifpw  7715  f1opwfi  7716  fival  7763  fi0  7771  dffi2  7774  elfiun  7781  cantnfp1lem1  7987  cantnfp1lem3  7989  cantnfp1lem1OLD  8013  cantnfp1lem3OLD  8015  epfrs  8052  r1fin  8081  r1tr  8084  r1ordg  8086  r1ord3g  8087  r1val1  8094  tz9.12lem3  8097  tcrank  8192  cplem1  8197  hta  8205  tskwe  8221  cardprclem  8250  r0weon  8280  fodomfi2  8331  alephfplem3  8377  dfac12r  8416  ackbij1lem6  8495  ackbij1lem9  8498  ackbij1lem10  8499  ackbij1lem11  8500  ackbij1lem16  8505  ackbij1lem18  8507  ackbij2  8513  fin23lem24  8592  fin23lem26  8595  fin23lem28  8610  fin23lem30  8612  fin23lem31  8613  isfin1-3  8656  fin1a2lem6  8675  hsmexlem4  8699  hsmexlem5  8700  hsmexlem6  8701  axdc2lem  8718  axdc3lem2  8721  axcclem  8727  ac6num  8749  brdom5  8797  brdom4  8798  canthp1lem2  8921  r1tskina  9050  gruina  9086  grur1a  9087  pinn  9148  0nnq  9194  elpqn  9195  recn  9473  rexr  9530  dedekindle  9635  ltord1  9967  leord1  9968  eqord1  9969  nnre  10430  nncn  10431  nnind  10441  nnnn0  10687  nn0re  10689  nn0cn  10690  nnz  10769  nn0z  10770  nnq  11067  qcn  11068  rpre  11098  difreicc  11518  iccshftri  11521  iccshftli  11523  iccdili  11525  icccntri  11527  fzval2  11541  fzelp1  11608  4fvwrd4  11634  elfzo1  11696  expcllem  11977  expcl2lem  11978  m1expcl2  11988  bcm1k  12192  bcpasc  12198  hashbclem  12307  swrd0fv0  12438  swrd0fvlsw  12441  seqshft  12676  sqrlem5  12838  cau3lem  12944  caubnd  12948  climconst2  13128  rlimres  13138  lo1res  13139  lo1resb  13144  rlimresb  13145  o1resb  13146  o1of2  13192  o1rlimmul  13198  caurcvg  13256  caucvg  13258  ackbijnn  13393  binomlem  13394  incexclem  13401  divalglem8  13706  sadadd  13765  smueqlem  13788  smumul  13791  isprm3  13874  phimullem  13956  prmdiveq  13963  unbenlem  14071  prmreclem2  14080  prmrec  14085  vdwnnlem1  14158  vdwnnlem3  14160  ramtcl2  14174  cshwshashlem1  14224  isstruct2  14285  structcnvcnv  14287  fvsetsid  14301  strlemor1  14367  imasdsval2  14556  xpsfrnel2  14605  mreunirn  14641  mrcfval  14648  mrisval  14670  isacs2  14693  acsfn  14699  homarcl  14998  arwval  15013  coafval  15034  coapm  15041  isdrs2  15211  isacs3lem  15438  psssdm2  15487  tsrss  15495  submnd0  15553  nmzsubg  15824  nmznsg  15827  resscntz  15951  cntzmhm  15958  symgtrinv  16080  pmtrdifellem4  16087  psgnpmtr  16118  efginvrel2  16328  efginvrel1  16329  efgsp1  16338  efgsres  16339  efgsfo  16340  frgpinv  16365  frgpupf  16374  frgpup1  16376  subcmn  16425  torsubg  16440  dprd2dlem1  16645  dpjidcl  16662  dpjidclOLD  16669  ablfaclem3  16693  subrgpropd  17005  lssacs  17154  sralmod  17374  psrbaglefi  17547  psrbaglefiOLD  17548  mplsubglem  17617  mplsubglemOLD  17619  ressmpladd  17643  ressmplmul  17644  ressmplvsca  17645  mplmonmul  17650  mplind  17691  ply1bascl  17766  cnsubdrglem  17973  rege0subm  17978  rge0srg  17991  zringunit  18023  zrngunit  18024  znrrg  18107  psgnghm  18119  zrhpsgnevpm  18130  evpmodpmf1o  18135  pmtrodpm  18136  frlmsslsp  18332  frlmsslspOLD  18333  islinds4  18373  lmimlbs  18374  lbslcic  18379  mdetralt  18530  mdetunilem7  18540  basdif0  18674  tgval2  18677  mreclatdemoBAD  18816  ordtbas  18912  ordtrest  18922  ordtrestixx  18942  fincmp  19112  cmpfi  19127  bwth  19129  iuncon  19148  1stcrest  19173  hauslly  19212  kgentop  19231  ptbasin  19266  ptcnplem  19310  txkgen  19341  infil  19552  filunirn  19571  uzrest  19586  elflim  19660  hauspwpwf1  19676  flffval  19678  fclsval  19697  isfcls  19698  fcfval  19722  alexsubALTlem3  19737  alexsubALTlem4  19738  ustn0  19911  fmucndlem  19982  xmetunirn  20028  blbas  20121  blres  20122  mopnval  20129  setsmstopn  20169  tmsval  20172  tngtopn  20352  qtopbaslem  20453  xrtgioo  20499  reperflem  20511  icccmplem1  20515  reconnlem2  20520  xrge0tsms  20527  icopnfhmeo  20631  icccvx  20638  bndth  20646  reparphti  20685  pcofval  20698  pcoval1  20701  pcoval2  20704  pcoass  20712  pcorevlem  20714  pcorev2  20716  pi1xfrcnv  20745  nmhmcn  20791  csscld  20877  cfilfval  20891  caufval  20902  cfilres  20923  bcthlem1  20951  ivthlem1  21051  ivthlem3  21053  ovolicc2lem3  21118  ovolicc2lem4  21119  ioombl1lem4  21158  vitalilem1  21204  mbflimsup  21260  i1fima2  21273  i1fd  21275  i1f0  21281  i1f1  21284  itg1addlem4  21293  itg1addlem5  21294  itg2cnlem2  21356  iblmbf  21361  ellimc2  21468  limcres  21477  limcun  21486  dvbsss  21493  perfdvf  21494  dvres2lem  21501  dvaddbr  21528  rolle  21578  cmvth  21579  dvlip  21581  dvlipcn  21582  dvle  21595  lhop1lem  21601  dvfsumle  21609  dvfsumge  21610  dvfsumabs  21611  dvfsumlem2  21615  ftc2  21632  itgparts  21635  itgsubstlem  21636  itgsubst  21637  deg1mul3  21703  coeval  21807  coeeu  21809  dgrval  21812  coef3  21816  coemulc  21838  dgrsub  21855  coecj  21861  dvply2  21868  dvnply  21870  quotval  21874  fta1  21890  plyexmo  21895  aacjcl  21909  taylfval  21940  dvtaylp  21951  abelth  22022  pilem2  22033  pilem3  22034  sinord  22106  recosf1o  22107  resinf1o  22108  tanord1  22109  eff1olem  22120  dvloglem  22209  dvlog  22212  dvlog2lem  22213  advlogexp  22216  logtayl  22221  logtayl2  22223  cxpcn3lem  22301  cxpcn3  22302  sqrcn  22304  loglesqr  22312  1cubr  22353  acosrecl  22414  rlimcnp2  22476  xrlimcnp  22478  efrlim  22479  jensen  22498  basellem4  22537  ppiprm  22605  chtprm  22607  prmorcht  22632  dvdsflip  22638  musum  22647  chpchtsum  22674  dchrinvcl  22708  dchrghm  22711  dchrinv  22716  dchrsum2  22723  dchrsum  22724  rplogsumlem2  22850  rpvmasumlem  22852  dchrisum0re  22878  dchrisum0lem2a  22882  dirith2  22893  pnt  22979  tglng  23099  axlowdimlem5  23327  axlowdimlem6  23328  axlowdimlem7  23329  axlowdimlem15  23337  axlowdimlem16  23338  axlowdimlem17  23339  axlowdim  23342  axeuclidlem  23343  axcontlem2  23346  axcontlem7  23351  axcontlem8  23352  issubgoi  23932  opidon  23944  flddivrng  24037  rngosn3  24048  vcoprnelem  24091  nvvcop  24107  nvex  24124  phnv  24349  sheli  24751  cheli  24770  choc1  24865  shintcli  24867  chintcli  24869  shsleji  24908  pjini  25237  mayete3i  25266  mayete3iOLD  25267  dmadjop  25427  nlelshi  25599  cnlnadjeui  25616  cnlnssadj  25619  bdopadj  25621  pjimai  25715  stcl  25755  atelch  25883  disjin  26063  fcnvgreu  26125  partfun  26127  f1od2  26158  fcobijfs  26160  xrge0infss  26187  iundisj2fi  26215  nnindf  26223  eliccioo  26240  xrsmulgzz  26273  xrge0mulgnn0  26284  xrge0nre  26287  xrge0omnd  26308  xrge0tsmsd  26387  prsdm  26478  prsrn  26479  ordtrestNEW  26485  xrge0iifcnv  26497  xrge0iifcv  26498  xrge0iifiso  26499  xrge0iifhom  26501  qqhcn  26554  rnlogblem  26592  esumval  26634  gsumesum  26644  esumlub  26645  esumcst  26648  esumfsup  26653  issgon  26700  elrnsiga  26703  imambfm  26811  br2base  26818  sxbrsigalem0  26820  dya2iocucvr  26833  sxbrsigalem2  26835  sxbrsigalem5  26837  sxbrsiga  26839  sibfof  26860  oddpwdc  26871  eulerpartlemelr  26874  eulerpartgbij  26889  eulerpartlemgvv  26893  eulerpartlemgh  26895  eulerpartlemgs2  26897  eulerpartlemn  26898  sseqf  26909  ballotlem2  27005  ballotlemfp1  27008  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemfmpn  27011  ballotlemsup  27021  ballotlemfrceq  27045  signswch  27096  lgamgulmlem2  27150  lgamucov2  27159  subfacp1lem5  27206  cvmsi  27288  divcnvshft  27532  zprod  27584  risefaccllem  27650  fallfaccllem  27651  dfon2lem4  27733  wfrlem4  27861  wfrlem10  27867  frrlem4  27905  pprodss4v  28049  linedegen  28308  bpolydiflem  28331  bpoly4  28336  nnssi2  28435  nnssi3  28436  sin2h  28560  cos2h  28561  tan2h  28562  heicant  28564  mblfinlem1  28566  cnambfre  28578  dvtan  28580  itg2addnc  28584  itg2gt0cn  28585  ftc1cnnc  28604  ftc2nc  28614  dvcncxp1  28615  dvcnsqr  28616  dvasin  28618  dvacos  28619  ivthALT  28668  neibastop2lem  28719  cover2  28745  opelopab3  28748  sstotbnd2  28811  heibor1lem  28846  heiborlem10  28857  exidcl  28879  elrfi  29168  elrfirn  29169  elrfirn2  29170  mrefg3  29182  diophin  29249  diophun  29250  eq0rabdioph  29253  eqrabdioph  29254  pellex  29314  rmxycomplete  29396  rmxypos  29428  ltrmynn0  29429  jm2.23  29483  aomclem2  29546  fglmod  29564  lsmfgcl  29565  lmhmfgima  29575  lmhmfgsplit  29577  isnumbasabl  29600  dgrsub2  29629  itgocn  29659  acsfn1p  29694  areaquad  29730  itgsin0pilem1  29928  itgsinexplem1  29932  itgsinexp  29933  stoweidlem34  29967  stoweidlem41  29974  stoweidlem51  29984  wallispilem2  29999  stirlinglem11  30017  elfvmptrab1  30292  2wlkonot3v  30532  2spthonot3v  30533  clwwlknprop  30573  clwwisshclww  30609  chfacfpmmulgsum2  31319  onfrALTlem2  31554  onfrALTlem2VD  31925  bnj1533  32145  bnj1137  32286  bnj1286  32310  bnj1408  32327  bnj1417  32332  bj-sngltagi  32775  bj-elid  32826  bj-elid2  32827  bj-flbi3  32833  bj-cmnssmndel  32879  bj-ablssgrpel  32881  bj-ablsscmnel  32883  bj-vecssmodel  32886  bj-rrvecssvecel  32893  bj-rrvecsscmnel  32895  toycom  32924  osumcllem7N  33912  pexmidlem4N  33923  diaintclN  35009  dibintclN  35118  mapd1o  35599  hdmapevec  35789  taupilemrplb  35920
  Copyright terms: Public domain W3C validator