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

Theorem sseli 3340
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 3338 . 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 1755    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  sselii  3341  sseldi  3342  elun1  3511  elun2  3512  copsex2ga  4938  issref  5199  2elresin  5510  nfvres  5708  fvco4i  5757  fvmptss  5770  fvmptex  5772  fvmptnf  5779  fvopab4ndm  5782  fvimacnvi  5805  elpreima  5811  iinpreima  5821  ofrfval  6317  ofval  6318  off  6323  nnon  6471  finds  6491  finds2  6493  offres  6561  eqopi  6599  op1steq  6607  dfoprab4  6620  bropopvvv  6642  curry1val  6654  curry2val  6658  reldmtpos  6742  smores3  6800  smores2  6801  frsuc  6878  nnfi  7491  unifpw  7602  f1opwfi  7603  fival  7650  fi0  7658  dffi2  7661  elfiun  7668  cantnfp1lem1  7874  cantnfp1lem3  7876  cantnfp1lem1OLD  7900  cantnfp1lem3OLD  7902  epfrs  7939  r1fin  7968  r1tr  7971  r1ordg  7973  r1ord3g  7974  r1val1  7981  tz9.12lem3  7984  tcrank  8079  cplem1  8084  hta  8092  tskwe  8108  cardprclem  8137  r0weon  8167  fodomfi2  8218  alephfplem3  8264  dfac12r  8303  ackbij1lem6  8382  ackbij1lem9  8385  ackbij1lem10  8386  ackbij1lem11  8387  ackbij1lem16  8392  ackbij1lem18  8394  ackbij2  8400  fin23lem24  8479  fin23lem26  8482  fin23lem28  8497  fin23lem30  8499  fin23lem31  8500  isfin1-3  8543  fin1a2lem6  8562  hsmexlem4  8586  hsmexlem5  8587  hsmexlem6  8588  axdc2lem  8605  axdc3lem2  8608  axcclem  8614  ac6num  8636  brdom5  8684  brdom4  8685  canthp1lem2  8808  r1tskina  8937  gruina  8973  grur1a  8974  pinn  9035  0nnq  9081  elpqn  9082  recn  9360  rexr  9417  dedekindle  9522  ltord1  9854  leord1  9855  eqord1  9856  nnre  10317  nncn  10318  nnind  10328  nnnn0  10574  nn0re  10576  nn0cn  10577  nnz  10656  nn0z  10657  nnq  10954  qcn  10955  rpre  10985  difreicc  11404  iccshftri  11407  iccshftli  11409  iccdili  11411  icccntri  11413  fzval2  11427  fzelp1  11492  4fvwrd4  11517  elfzo1  11579  expcllem  11860  expcl2lem  11861  m1expcl2  11871  bcm1k  12075  bcpasc  12081  hashbclem  12189  swrd0fv0  12320  swrd0fvlsw  12323  seqshft  12558  sqrlem5  12720  cau3lem  12826  caubnd  12830  climconst2  13010  rlimres  13020  lo1res  13021  lo1resb  13026  rlimresb  13027  o1resb  13028  o1of2  13074  o1rlimmul  13080  caurcvg  13138  caucvg  13140  ackbijnn  13274  binomlem  13275  incexclem  13282  divalglem8  13587  sadadd  13646  smueqlem  13669  smumul  13672  isprm3  13755  phimullem  13837  prmdiveq  13844  unbenlem  13952  prmreclem2  13961  prmrec  13966  vdwnnlem1  14039  vdwnnlem3  14041  ramtcl2  14055  cshwshashlem1  14105  isstruct2  14166  structcnvcnv  14168  fvsetsid  14182  strlemor1  14248  imasdsval2  14437  xpsfrnel2  14486  mreunirn  14522  mrcfval  14529  mrisval  14551  isacs2  14574  acsfn  14580  homarcl  14879  arwval  14894  coafval  14915  coapm  14922  isdrs2  15092  isacs3lem  15319  psssdm2  15368  tsrss  15376  submnd0  15434  nmzsubg  15702  nmznsg  15705  resscntz  15829  cntzmhm  15836  symgtrinv  15958  pmtrdifellem4  15965  psgnpmtr  15996  efginvrel2  16204  efginvrel1  16205  efgsp1  16214  efgsres  16215  efgsfo  16216  frgpinv  16241  frgpupf  16250  frgpup1  16252  subcmn  16301  torsubg  16316  dprd2dlem1  16514  dpjidcl  16531  dpjidclOLD  16538  ablfaclem3  16562  subrgpropd  16823  lssacs  16970  sralmod  17190  psrbaglefi  17375  psrbaglefiOLD  17376  mplsubglem  17444  mplsubglemOLD  17446  ressmpladd  17470  ressmplmul  17471  ressmplvsca  17472  mplmonmul  17477  mplind  17516  ply1bascl  17558  cnsubdrglem  17708  rege0subm  17713  zringunit  17756  zrngunit  17757  znrrg  17840  psgnghm  17852  zrhpsgnevpm  17863  evpmodpmf1o  17868  pmtrodpm  17869  frlmsslsp  18065  frlmsslspOLD  18066  islinds4  18106  lmimlbs  18107  lbslcic  18112  mdetralt  18256  mdetunilem7  18266  basdif0  18400  tgval2  18403  mreclatdemoBAD  18542  ordtbas  18638  ordtrest  18648  ordtrestixx  18668  fincmp  18838  cmpfi  18853  bwth  18855  iuncon  18874  1stcrest  18899  hauslly  18938  kgentop  18957  ptbasin  18992  ptcnplem  19036  txkgen  19067  infil  19278  filunirn  19297  uzrest  19312  elflim  19386  hauspwpwf1  19402  flffval  19404  fclsval  19423  isfcls  19424  fcfval  19448  alexsubALTlem3  19463  alexsubALTlem4  19464  ustn0  19637  fmucndlem  19708  xmetunirn  19754  blbas  19847  blres  19848  mopnval  19855  setsmstopn  19895  tmsval  19898  tngtopn  20078  qtopbaslem  20179  xrtgioo  20225  reperflem  20237  icccmplem1  20241  reconnlem2  20246  xrge0tsms  20253  icopnfhmeo  20357  icccvx  20364  bndth  20372  reparphti  20411  pcofval  20424  pcoval1  20427  pcoval2  20430  pcoass  20438  pcorevlem  20440  pcorev2  20442  pi1xfrcnv  20471  nmhmcn  20517  csscld  20603  cfilfval  20617  caufval  20628  cfilres  20649  bcthlem1  20677  ivthlem1  20777  ivthlem3  20779  ovolicc2lem3  20844  ovolicc2lem4  20845  ioombl1lem4  20884  vitalilem1  20930  mbflimsup  20986  i1fima2  20999  i1fd  21001  i1f0  21007  i1f1  21010  itg1addlem4  21019  itg1addlem5  21020  itg2cnlem2  21082  iblmbf  21087  ellimc2  21194  limcres  21203  limcun  21212  dvbsss  21219  perfdvf  21220  dvres2lem  21227  dvaddbr  21254  rolle  21304  cmvth  21305  dvlip  21307  dvlipcn  21308  dvle  21321  lhop1lem  21327  dvfsumle  21335  dvfsumge  21336  dvfsumabs  21337  dvfsumlem2  21341  ftc2  21358  itgparts  21361  itgsubstlem  21362  itgsubst  21363  deg1mul3  21472  coeval  21576  coeeu  21578  dgrval  21581  coef3  21585  coemulc  21607  dgrsub  21624  coecj  21630  dvply2  21637  dvnply  21639  quotval  21643  fta1  21659  plyexmo  21664  aacjcl  21678  taylfval  21709  dvtaylp  21720  abelth  21791  pilem2  21802  pilem3  21803  sinord  21875  recosf1o  21876  resinf1o  21877  tanord1  21878  eff1olem  21889  dvloglem  21978  dvlog  21981  dvlog2lem  21982  advlogexp  21985  logtayl  21990  logtayl2  21992  cxpcn3lem  22070  cxpcn3  22071  sqrcn  22073  loglesqr  22081  1cubr  22122  acosrecl  22183  rlimcnp2  22245  xrlimcnp  22247  efrlim  22248  jensen  22267  basellem4  22306  ppiprm  22374  chtprm  22376  prmorcht  22401  dvdsflip  22407  musum  22416  chpchtsum  22443  dchrinvcl  22477  dchrghm  22480  dchrinv  22485  dchrsum2  22492  dchrsum  22493  rplogsumlem2  22619  rpvmasumlem  22621  dchrisum0re  22647  dchrisum0lem2a  22651  dirith2  22662  pnt  22748  tglng  22861  axlowdimlem5  23015  axlowdimlem6  23016  axlowdimlem7  23017  axlowdimlem15  23025  axlowdimlem16  23026  axlowdimlem17  23027  axlowdim  23030  axeuclidlem  23031  axcontlem2  23034  axcontlem7  23039  axcontlem8  23040  issubgoi  23620  opidon  23632  flddivrng  23725  rngosn3  23736  vcoprnelem  23779  nvvcop  23795  nvex  23812  phnv  24037  sheli  24439  cheli  24458  choc1  24553  shintcli  24555  chintcli  24557  shsleji  24596  pjini  24925  mayete3i  24954  mayete3iOLD  24955  dmadjop  25115  nlelshi  25287  cnlnadjeui  25304  cnlnssadj  25307  bdopadj  25309  pjimai  25403  stcl  25443  atelch  25571  disjin  25753  fcnvgreu  25815  partfun  25817  f1od2  25848  fcobijfs  25850  iundisj2fi  25904  nnindf  25912  eliccioo  25929  xrsmulgzz  25962  xrge0mulgnn0  25973  xrge0nre  25976  xrge0omnd  25998  rge0srg  26064  xrge0tsmsd  26106  prsdm  26198  prsrn  26199  ordtrestNEW  26205  xrge0iifcnv  26217  xrge0iifcv  26218  xrge0iifiso  26219  xrge0iifhom  26221  qqhcn  26274  rnlogblem  26312  esumval  26354  gsumesum  26364  esumlub  26365  esumcst  26368  esumfsup  26373  issgon  26420  elrnsiga  26423  imambfm  26531  br2base  26538  sxbrsigalem0  26540  dya2iocucvr  26553  sxbrsigalem2  26555  sxbrsigalem5  26557  sxbrsiga  26559  sibfof  26574  oddpwdc  26585  eulerpartlemelr  26588  eulerpartgbij  26603  eulerpartlemgvv  26607  eulerpartlemgh  26609  eulerpartlemgs2  26611  eulerpartlemn  26612  sseqf  26623  ballotlem2  26719  ballotlemfp1  26722  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemfmpn  26725  ballotlemsup  26735  ballotlemfrceq  26759  signswch  26810  lgamgulmlem2  26864  lgamucov2  26873  subfacp1lem5  26920  cvmsi  27002  divcnvshft  27245  zprod  27297  risefaccllem  27363  fallfaccllem  27364  dfon2lem4  27446  wfrlem4  27574  wfrlem10  27580  frrlem4  27618  pprodss4v  27762  linedegen  28021  bpolydiflem  28044  bpoly4  28049  nnssi2  28149  nnssi3  28150  sin2h  28266  cos2h  28267  tan2h  28268  heicant  28270  mblfinlem1  28272  cnambfre  28284  dvtan  28286  itg2addnc  28290  itg2gt0cn  28291  ftc1cnnc  28310  ftc2nc  28320  dvcncxp1  28321  dvcnsqr  28322  dvasin  28324  dvacos  28325  ivthALT  28374  neibastop2lem  28425  cover2  28451  opelopab3  28454  sstotbnd2  28517  heibor1lem  28552  heiborlem10  28563  exidcl  28585  elrfi  28875  elrfirn  28876  elrfirn2  28877  mrefg3  28889  diophin  28956  diophun  28957  eq0rabdioph  28960  eqrabdioph  28961  pellex  29021  rmxycomplete  29103  rmxypos  29135  ltrmynn0  29136  jm2.23  29190  aomclem2  29253  fglmod  29271  lsmfgcl  29272  lmhmfgima  29282  lmhmfgsplit  29284  isnumbasabl  29307  dgrsub2  29336  itgocn  29366  acsfn1p  29401  areaquad  29437  itgsin0pilem1  29636  itgsinexplem1  29640  itgsinexp  29641  stoweidlem34  29675  stoweidlem41  29682  stoweidlem51  29692  wallispilem2  29707  stirlinglem11  29725  elfvmptrab1  30000  2wlkonot3v  30240  2spthonot3v  30241  clwwlknprop  30281  clwwisshclww  30317  onfrALTlem2  30955  onfrALTlem2VD  31327  bnj1533  31547  bnj1137  31688  bnj1286  31712  bnj1408  31729  bnj1417  31734  bj-sngltagi  32058  bj-elid  32101  bj-flbi3  32107  bj-vecmoda  32153  bj-abelcmnda  32156  bj-rrveccmnda  32164  toycom  32191  osumcllem7N  33179  pexmidlem4N  33190  diaintclN  34276  dibintclN  34385  mapd1o  34866  hdmapevec  35056  taupilemrplb  35187
  Copyright terms: Public domain W3C validator