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

Theorem sseli 3304
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 3302 . 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 1721    C_ wss 3280
This theorem is referenced by:  sselii  3305  sseldi  3306  elun1  3474  elun2  3475  nnon  4810  finds  4830  finds2  4832  issref  5206  2elresin  5515  nfvres  5719  fvco4i  5760  fvmptss  5772  fvmptex  5774  fvmptnf  5781  fvopab4ndm  5784  fvimacnvi  5803  elpreima  5809  iinpreima  5819  ofrfval  6272  ofval  6273  offres  6278  off  6279  eqopi  6342  op1steq  6350  dfoprab4  6363  copsex2ga  6367  bropopvvv  6385  curry1val  6398  curry2val  6402  reldmtpos  6446  smores3  6574  smores2  6575  frsuc  6653  nnfi  7258  unifpw  7367  f1opwfi  7368  fival  7375  fi0  7383  dffi2  7386  elfiun  7393  cantnfp1lem1  7590  cantnfp1lem3  7592  epfrs  7623  r1fin  7655  r1tr  7658  r1ordg  7660  r1ord3g  7661  r1val1  7668  tz9.12lem3  7671  tcrank  7764  cplem1  7769  hta  7777  tskwe  7793  cardprclem  7822  r0weon  7850  fodomfi2  7897  alephfplem3  7943  dfac12r  7982  ackbij1lem6  8061  ackbij1lem9  8064  ackbij1lem10  8065  ackbij1lem11  8066  ackbij1lem16  8071  ackbij1lem18  8073  ackbij2  8079  fin23lem24  8158  fin23lem26  8161  fin23lem28  8176  fin23lem30  8178  fin23lem31  8179  isfin1-3  8222  fin1a2lem6  8241  hsmexlem4  8265  hsmexlem5  8266  hsmexlem6  8267  axdc2lem  8284  axdc3lem2  8287  axcclem  8293  ac6num  8315  brdom5  8363  brdom4  8364  canthp1lem2  8484  r1tskina  8613  gruina  8649  grur1a  8650  pinn  8711  0nnq  8757  elpqn  8758  recn  9036  rexr  9086  ltord1  9509  leord1  9510  eqord1  9511  nnre  9963  nncn  9964  nnind  9974  nnnn0  10184  nn0re  10186  nn0cn  10187  nnz  10259  nn0z  10260  nnq  10543  qcn  10544  rpre  10574  difreicc  10984  iccshftri  10987  iccshftli  10989  iccdili  10991  icccntri  10993  fzval2  11002  fzelp1  11055  4fvwrd4  11076  elfzo1  11128  expcllem  11347  expcl2lem  11348  m1expcl2  11358  bcm1k  11561  bcpasc  11567  hashbclem  11656  seqshft  11855  sqrlem5  12007  cau3lem  12113  caubnd  12117  climconst2  12297  rlimres  12307  lo1res  12308  lo1resb  12313  rlimresb  12314  o1resb  12315  o1of2  12361  o1rlimmul  12367  caurcvg  12425  caucvg  12427  zsum  12467  ackbijnn  12562  binomlem  12563  incexclem  12571  divalglem8  12875  sadadd  12934  smueqlem  12957  smumul  12960  isprm3  13043  phimullem  13123  prmdiveq  13130  unbenlem  13231  prmreclem2  13240  prmrec  13245  vdwnnlem1  13318  vdwnnlem3  13320  ramtcl2  13334  isstruct2  13433  structcnvcnv  13435  strlemor1  13511  imasdsval2  13697  xpsfrnel2  13745  mreunirn  13781  mrcfval  13788  mrisval  13810  isacs2  13833  acsfn  13839  homarcl  14138  arwval  14153  coafval  14174  coapm  14181  isdrs2  14351  isacs3lem  14547  psssdm2  14602  tsrss  14610  submnd0  14680  nmzsubg  14936  nmznsg  14939  resscntz  15085  cntzmhm  15092  efginvrel2  15314  efginvrel1  15315  efgsp1  15324  efgsres  15325  efgsfo  15326  frgpinv  15351  frgpupf  15360  frgpup1  15362  subcmn  15411  torsubg  15424  dprd2dlem1  15554  dpjidcl  15571  ablfaclem3  15600  subrgpropd  15857  lssacs  15998  sralmod  16213  psrbaglefi  16392  mplsubglem  16453  ressmpladd  16475  ressmplmul  16476  ressmplvsca  16477  mplmonmul  16482  mplind  16517  ply1bascl  16556  cnsubdrglem  16704  rege0subm  16710  zrngunit  16720  znrrg  16801  basdif0  16973  tgval2  16976  mreclatdemo  17115  ordtbas  17210  ordtrest  17220  ordtrestixx  17240  fincmp  17410  cmpfi  17425  iuncon  17444  1stcrest  17469  hauslly  17508  kgentop  17527  ptbasin  17562  ptcnplem  17606  txkgen  17637  infil  17848  filunirn  17867  uzrest  17882  elflim  17956  hauspwpwf1  17972  flffval  17974  fclsval  17993  isfcls  17994  fcfval  18018  alexsubALTlem3  18033  alexsubALTlem4  18034  ustn0  18203  fmucndlem  18274  xmetunirn  18320  blbas  18413  blres  18414  mopnval  18421  setsmstopn  18461  tmsval  18464  tngtopn  18644  qtopbaslem  18745  xrtgioo  18790  reperflem  18802  icccmplem1  18806  reconnlem2  18811  xrge0tsms  18818  icopnfhmeo  18921  icccvx  18928  bndth  18936  reparphti  18975  pcofval  18988  pcoval1  18991  pcoval2  18994  pcoass  19002  pcorevlem  19004  pcorev2  19006  pi1xfrcnv  19035  nmhmcn  19081  csscld  19156  cfilfval  19170  caufval  19181  cfilres  19202  bcthlem1  19230  ivthlem1  19301  ivthlem3  19303  ovolicc2lem3  19368  ovolicc2lem4  19369  ioombl1lem4  19408  vitalilem1  19453  mbflimsup  19511  i1fima2  19524  i1fd  19526  i1f0  19532  i1f1  19535  itg1addlem4  19544  itg1addlem5  19545  itg2cnlem2  19607  iblmbf  19612  ellimc2  19717  limcres  19726  limcun  19735  dvbsss  19742  perfdvf  19743  dvres2lem  19750  dvaddbr  19777  rolle  19827  cmvth  19828  dvlip  19830  dvlipcn  19831  dvle  19844  lhop1lem  19850  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem2  19864  ftc2  19881  itgparts  19884  itgsubstlem  19885  itgsubst  19886  deg1mul3  19991  coeval  20095  coeeu  20097  dgrval  20100  coef3  20104  coemulc  20126  dgrsub  20143  coecj  20149  dvply2  20156  dvnply  20158  quotval  20162  fta1  20178  plyexmo  20183  aacjcl  20197  taylfval  20228  dvtaylp  20239  abelth  20310  pilem2  20321  pilem3  20322  sinord  20389  recosf1o  20390  resinf1o  20391  tanord1  20392  eff1olem  20403  dvloglem  20492  dvlog  20495  dvlog2lem  20496  advlogexp  20499  logtayl  20504  logtayl2  20506  cxpcn3lem  20584  cxpcn3  20585  sqrcn  20587  loglesqr  20595  1cubr  20635  acosrecl  20696  rlimcnp2  20758  xrlimcnp  20760  efrlim  20761  jensen  20780  basellem4  20819  ppiprm  20887  chtprm  20889  prmorcht  20914  dvdsflip  20920  musum  20929  chpchtsum  20956  dchrinvcl  20990  dchrghm  20993  dchrinv  20998  dchrsum2  21005  dchrsum  21006  rplogsumlem2  21132  rpvmasumlem  21134  dchrisum0re  21160  dchrisum0lem2a  21164  dirith2  21175  pnt  21261  issubgoi  21851  opidon  21863  flddivrng  21956  rngosn3  21967  vcoprnelem  22010  nvvcop  22026  nvex  22043  phnv  22268  sheli  22669  cheli  22688  choc1  22782  shintcli  22784  chintcli  22786  shsleji  22825  pjini  23154  mayete3i  23183  mayete3iOLD  23184  dmadjop  23344  nlelshi  23516  cnlnadjeui  23533  cnlnssadj  23536  bdopadj  23538  pjimai  23632  stcl  23672  atelch  23800  disjin  23980  partfun  24040  iundisj2fi  24106  eliccioo  24130  xrsmulgzz  24153  xrge0mulgnn0  24163  xrge0nre  24166  xrge0tsmsd  24176  xrge0iifcnv  24272  xrge0iifcv  24273  xrge0iifiso  24274  xrge0iifhom  24276  qqhcn  24328  rnlogblem  24352  esumval  24394  gsumesum  24404  esumlub  24405  esumcst  24408  esumfsup  24413  issgon  24459  elrnsiga  24462  imambfm  24565  br2base  24572  sxbrsigalem0  24574  dya2iocucvr  24587  sxbrsigalem2  24589  sxbrsigalem5  24591  sxbrsiga  24593  sibfof  24607  sitmcl  24616  ballotlem2  24699  ballotlemfp1  24702  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemfmpn  24705  ballotlemsup  24715  ballotlemfrceq  24739  lgamgulmlem2  24767  lgamucov2  24776  subfacp1lem5  24823  cvmsi  24905  dedekindle  25141  divcnvshft  25164  zprod  25216  risefaccllem  25281  fallfaccllem  25282  binomfallfaclem2  25307  dfon2lem4  25356  wfrlem4  25473  wfrlem10  25479  frrlem4  25498  pprodss4v  25638  axlowdimlem5  25789  axlowdimlem6  25790  axlowdimlem7  25791  axlowdimlem15  25799  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  axeuclidlem  25805  axcontlem2  25808  axcontlem7  25813  axcontlem8  25814  linedegen  25981  bpolydiflem  26004  bpoly4  26009  nnssi2  26109  nnssi3  26110  mblfinlem  26143  cnambfre  26154  itg2addnc  26158  itg2gt0cn  26159  ftc1cnnc  26178  ivthALT  26228  neibastop2lem  26279  cover2  26305  opelopab3  26308  sstotbnd2  26373  heibor1lem  26408  heiborlem10  26419  exidcl  26441  elrfi  26638  elrfirn  26639  elrfirn2  26640  mrefg3  26652  diophin  26721  diophun  26722  eq0rabdioph  26725  eqrabdioph  26726  pellex  26788  rmxycomplete  26870  rmxypos  26902  ltrmynn0  26903  jm2.23  26957  aomclem2  27020  fglmod  27039  lsmfgcl  27040  lmhmfgima  27050  lmhmfgsplit  27052  frlmsslsp  27116  isnumbasabl  27139  islinds4  27173  lmimlbs  27174  lbslcic  27179  dgrsub2  27207  itgocn  27237  symgtrinv  27281  psgnpmtr  27301  psgnghm  27305  acsfn1p  27375  itgsin0pilem1  27611  itgsinexplem1  27615  itgsinexp  27616  stoweidlem34  27650  stoweidlem41  27657  stoweidlem51  27667  wallispilem2  27682  stirlinglem11  27700  2wlkonot3v  28072  2spthonot3v  28073  onfrALTlem2  28343  onfrALTlem2VD  28710  bnj1533  28929  bnj1137  29070  bnj1286  29094  bnj1408  29111  bnj1417  29116  toycom  29455  osumcllem7N  30444  pexmidlem4N  30455  diaintclN  31541  dibintclN  31650  mapd1o  32131  hdmapevec  32321
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator