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

Theorem sseli 3176
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 3174 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
31, 2ax-mp 8 1  |-  ( C  e.  A  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684    C_ wss 3152
This theorem is referenced by:  sselii  3177  sseldi  3178  elun1  3342  elun2  3343  nnon  4662  finds  4682  finds2  4684  issref  5056  2elresin  5355  nfvres  5557  fvco4i  5597  fvmptss  5609  fvmptex  5610  fvmptnf  5617  fvopab4ndm  5620  fvimacnvi  5639  elpreima  5645  iinpreima  5655  ofrfval  6086  ofval  6087  offres  6092  off  6093  eqopi  6156  op1steq  6164  dfoprab4  6177  copsex2ga  6181  curry1val  6211  curry2val  6215  reldmtpos  6242  smores3  6370  smores2  6371  frsuc  6449  nnfi  7053  unifpw  7158  f1opwfi  7159  fival  7166  fi0  7173  dffi2  7176  elfiun  7183  cantnfp1lem1  7380  cantnfp1lem3  7382  epfrs  7413  r1fin  7445  r1tr  7448  r1ordg  7450  r1ord3g  7451  r1val1  7458  tz9.12lem3  7461  tcrank  7554  cplem1  7559  hta  7567  tskwe  7583  cardprclem  7612  r0weon  7640  fodomfi2  7687  alephfplem3  7733  dfac12r  7772  kmlem1  7776  ackbij1lem6  7851  ackbij1lem9  7854  ackbij1lem10  7855  ackbij1lem11  7856  ackbij1lem16  7861  ackbij1lem18  7863  ackbij2  7869  fin23lem24  7948  fin23lem26  7951  fin23lem28  7966  fin23lem30  7968  fin23lem31  7969  isfin1-3  8012  fin1a2lem6  8031  fin1a2lem9  8034  hsmexlem4  8055  hsmexlem5  8056  hsmexlem6  8057  axdc2lem  8074  axdc3lem2  8077  axcclem  8083  ac6num  8106  brdom5  8154  brdom4  8155  canthp1lem2  8275  r1tskina  8404  gruina  8440  grur1a  8441  pinn  8502  0nnq  8548  elpqn  8549  recn  8827  rexr  8877  ltord1  9299  leord1  9300  eqord1  9301  nnre  9753  nncn  9754  nnind  9764  nnnn0  9972  nn0re  9974  nn0cn  9975  nnz  10045  nn0z  10046  ublbneg  10302  nnq  10329  qcn  10330  rpre  10360  difreicc  10767  iccshftri  10770  iccshftli  10772  iccdili  10774  icccntri  10776  fzval2  10785  fzelp1  10838  expcllem  11114  expcl2lem  11115  m1expcl2  11125  bcm1k  11327  bcpasc  11333  hashbclem  11390  seqshft  11580  sqrlem5  11732  cau3lem  11838  caubnd  11842  climconst2  12022  rlimres  12032  lo1res  12033  lo1resb  12038  rlimresb  12039  o1resb  12040  rlimrege0  12053  o1of2  12086  o1rlimmul  12092  caurcvg  12149  caucvg  12151  zsum  12191  ackbijnn  12286  binomlem  12287  incexclem  12295  divalglem8  12599  sadadd  12658  smueqlem  12681  smumul  12684  isprm3  12767  phimullem  12847  prmdiveq  12854  unbenlem  12955  prmreclem2  12964  prmrec  12969  vdwnnlem1  13042  vdwnnlem3  13044  ramtcl2  13058  isstruct2  13157  structcnvcnv  13159  strlemor1  13235  imasdsval2  13419  xpsfrnel2  13467  mreunirn  13503  mrcfval  13510  mrisval  13532  isacs2  13555  acsfn  13561  homarcl  13860  arwval  13875  coafval  13896  coapm  13903  isdrs2  14073  isacs3lem  14269  psssdm2  14324  tsrss  14332  submnd0  14402  nmzsubg  14658  nmznsg  14661  resscntz  14807  cntzmhm  14814  odcl  14851  odlem2  14854  gexcl  14891  gexlem2  14893  gexdvds  14895  pgpssslw  14925  efginvrel2  15036  efginvrel1  15037  efgsp1  15046  efgsres  15047  efgsfo  15048  frgpinv  15073  frgpupf  15082  frgpup1  15084  subcmn  15133  torsubg  15146  dprd2dlem1  15276  dpjidcl  15293  ablfaclem3  15322  subrgpropd  15579  lssacs  15724  sralmod  15939  psrbaglefi  16118  resspsrmul  16161  mplsubglem  16179  ressmpladd  16201  ressmplmul  16202  ressmplvsca  16203  mplmonmul  16208  mplind  16243  ply1bascl  16284  psropprmul  16316  coe1mul2  16346  cnsubdrglem  16422  rege0subm  16428  zrngunit  16438  znrrg  16519  basdif0  16691  tgval2  16694  mreclatdemo  16833  ordtbas  16922  ordtrest  16932  ordtrestixx  16952  fincmp  17120  cmpfi  17135  iuncon  17154  1stcrest  17179  hauslly  17218  kgentop  17237  ptbasin  17272  ptcnplem  17315  txkgen  17346  infil  17558  filunirn  17577  uzrest  17592  elflim  17666  hauspwpwf1  17682  flffval  17684  fclsval  17703  isfcls  17704  fcfval  17728  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem3  17748  xmetunirn  17902  blfval  17947  blbas  17976  blres  17977  mopnval  17984  setsmstopn  18024  tmsval  18027  tngtopn  18166  qtopbaslem  18267  xrtgioo  18312  reperflem  18323  icccmplem1  18327  reconnlem2  18332  xrge0tsms  18339  icopnfhmeo  18441  icccvx  18448  bndth  18456  reparphti  18495  pcofval  18508  pcoval1  18511  pcoval2  18514  pcoass  18522  pcorevlem  18524  pcorev2  18526  pi1xfrcnv  18555  nmhmcn  18601  csscld  18676  cfilfval  18690  caufval  18701  cfilres  18722  bcthlem1  18746  ivthlem1  18811  ivthlem3  18813  ovolicc2lem3  18878  ovolicc2lem4  18879  ioombl1lem4  18918  vitalilem1  18963  mbflimsup  19021  i1fima2  19034  i1fd  19036  i1f0  19042  i1f1  19045  itg1addlem4  19054  itg1addlem5  19055  itg2cnlem2  19117  iblmbf  19122  ellimc2  19227  limcres  19236  limcun  19245  dvbsss  19252  perfdvf  19253  dvres2lem  19260  dvaddbr  19287  dvmulbr  19288  rolle  19337  cmvth  19338  dvlip  19340  dvlipcn  19341  dvle  19354  lhop1lem  19360  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvfsumlem2  19374  ftc2  19391  itgparts  19394  itgsubstlem  19395  itgsubst  19396  mdegmullem  19464  deg1mul3  19501  coeval  19605  coeeu  19607  dgrval  19610  coef3  19614  coemulc  19636  dgrsub  19653  coecj  19659  dvply2  19666  dvnply  19668  quotval  19672  fta1  19688  plyexmo  19693  aacjcl  19707  taylfval  19738  dvtaylp  19749  abelth  19817  pilem2  19828  pilem3  19829  sinord  19896  recosf1o  19897  resinf1o  19898  tanord1  19899  eff1olem  19910  dvloglem  19995  dvlog  19998  dvlog2lem  19999  advlogexp  20002  logtayl  20007  logtayl2  20009  cxpcn3lem  20087  cxpcn3  20088  sqrcn  20090  loglesqr  20098  1cubr  20138  acosrecl  20199  rlimcnp2  20261  xrlimcnp  20263  efrlim  20264  jensen  20283  basellem4  20321  0sgm  20382  sgmf  20383  sgmnncl  20385  ppiprm  20389  chtprm  20391  prmorcht  20416  dvdsflip  20422  fsumdvdscom  20425  dvdsppwf1o  20426  musum  20431  musumsum  20432  muinv  20433  sgmppw  20436  chpchtsum  20458  dchrinvcl  20492  dchrghm  20495  dchrinv  20500  dchrsum2  20507  dchrsum  20508  rplogsumlem2  20634  rpvmasumlem  20636  dchrmusum2  20643  dchrvmasumlem1  20644  dchrvmasum2lem  20645  dchrisum0fmul  20655  dchrisum0ff  20656  dchrisum0flblem1  20657  dchrisum0re  20662  dchrisum0lem2a  20666  dchrisum0  20669  dirith2  20677  logsqvma  20691  pnt  20763  issubgoi  20977  opidon  20989  flddivrng  21082  rngosn3  21093  vcoprnelem  21134  nvvcop  21150  nvex  21167  phnv  21392  sheli  21793  cheli  21812  choc1  21906  shintcli  21908  chintcli  21910  shsleji  21949  pjini  22278  mayete3i  22307  mayete3iOLD  22308  dmadjop  22468  nlelshi  22640  cnlnadjeui  22657  cnlnssadj  22660  bdopadj  22662  pjimai  22756  stcl  22796  atelch  22924  ballotlemfp1  23050  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemfmpn  23053  ballotlemsup  23063  ballotlemfrceq  23087  ballotlemirc  23090  eliccioo  23115  partfun  23240  elfzo1  23279  rmulccn  23301  xrsmulgzz  23307  xrge0mulgnn0  23313  xrge0iifcnv  23315  xrge0iifcv  23316  xrge0iifiso  23317  xrge0iifhom  23319  xrge0npcan  23333  disjin  23362  iundisj2fi  23364  xrge0tsmsd  23382  rnlogblem  23401  esumval  23425  esumel  23426  esumcst  23436  issgon  23484  elrnsiga  23487  measvunilem  23540  imambfm  23567  br2base  23574  probmeasb  23633  subfacp1lem5  23715  cvmsi  23796  dedekindle  24083  dfon2lem4  24142  wfrlem4  24259  wfrlem10  24265  frrlem4  24284  pprodss4v  24424  axlowdimlem5  24574  axlowdimlem6  24575  axlowdimlem7  24576  axlowdimlem15  24584  axlowdimlem16  24585  axlowdimlem17  24586  axlowdim  24589  axeuclidlem  24590  axcontlem2  24593  axcontlem7  24598  axcontlem8  24599  linedegen  24766  bpolydiflem  24789  bpoly4  24794  nnssi2  24894  nnssi3  24895  domintrefb  25063  mappow  25089  fvsnn  25114  elixp2b  25154  dstr  25171  posispre  25241  inposet  25278  reacomsmgrp1  25343  reacomsmgrp2  25344  reacomsmgrp3  25345  reacomsmgrp4  25346  clfsebsr  25349  resgcom  25351  basexre  25522  intopcoaconb  25540  iintlem2  25611  negveudr  25669  subclrvd  25674  issubcata  25846  inttaror  25900  smbkle  26043  pgapspf2  26053  ivthALT  26258  neibastop2lem  26309  cover2  26358  opelopab3  26373  sstotbnd2  26498  heibor1lem  26533  heiborlem10  26544  exidcl  26566  elrfi  26769  elrfirn  26770  elrfirn2  26771  mrefg3  26783  diophin  26852  diophun  26853  eq0rabdioph  26856  eqrabdioph  26857  rencldnfilem  26903  irrapx1  26913  pellex  26920  rmxycomplete  27002  rmxypos  27034  ltrmynn0  27035  jm2.23  27089  aomclem2  27152  fglmod  27171  lsmfgcl  27172  lmhmfgima  27182  lmhmfgsplit  27184  frlmsslsp  27248  isnumbasabl  27271  islinds4  27305  lmimlbs  27306  lbslcic  27311  dgrsub2  27339  itgocn  27369  symgtrinv  27413  psgnpmtr  27433  psgnghm  27437  acsfn1p  27507  phisum  27518  itgsin0pilem1  27744  itgsinexplem1  27748  itgsinexp  27749  stoweidlem15  27764  stoweidlem34  27783  stoweidlem51  27800  wallispilem2  27815  wallispi  27819  stirlinglem11  27833  onfrALTlem2  28311  onfrALTlem2VD  28665  bnj1533  28884  bnj110  28890  bnj1137  29025  bnj1286  29049  bnj1408  29066  bnj1417  29071  toycom  29162  osumcllem7N  30151  pexmidlem4N  30162  diaintclN  31248  dibintclN  31357  mapd1o  31838  hdmapevec  32028
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator