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

Theorem sseli 3189
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 3187 . 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 1696    C_ wss 3165
This theorem is referenced by:  sselii  3190  sseldi  3191  elun1  3355  elun2  3356  nnon  4678  finds  4698  finds2  4700  issref  5072  2elresin  5371  nfvres  5573  fvco4i  5613  fvmptss  5625  fvmptex  5626  fvmptnf  5633  fvopab4ndm  5636  fvimacnvi  5655  elpreima  5661  iinpreima  5671  ofrfval  6102  ofval  6103  offres  6108  off  6109  eqopi  6172  op1steq  6180  dfoprab4  6193  copsex2ga  6197  curry1val  6227  curry2val  6231  reldmtpos  6258  smores3  6386  smores2  6387  frsuc  6465  nnfi  7069  unifpw  7174  f1opwfi  7175  fival  7182  fi0  7189  dffi2  7192  elfiun  7199  cantnfp1lem1  7396  cantnfp1lem3  7398  epfrs  7429  r1fin  7461  r1tr  7464  r1ordg  7466  r1ord3g  7467  r1val1  7474  tz9.12lem3  7477  tcrank  7570  cplem1  7575  hta  7583  tskwe  7599  cardprclem  7628  r0weon  7656  fodomfi2  7703  alephfplem3  7749  dfac12r  7788  kmlem1  7792  ackbij1lem6  7867  ackbij1lem9  7870  ackbij1lem10  7871  ackbij1lem11  7872  ackbij1lem16  7877  ackbij1lem18  7879  ackbij2  7885  fin23lem24  7964  fin23lem26  7967  fin23lem28  7982  fin23lem30  7984  fin23lem31  7985  isfin1-3  8028  fin1a2lem6  8047  fin1a2lem9  8050  hsmexlem4  8071  hsmexlem5  8072  hsmexlem6  8073  axdc2lem  8090  axdc3lem2  8093  axcclem  8099  ac6num  8122  brdom5  8170  brdom4  8171  canthp1lem2  8291  r1tskina  8420  gruina  8456  grur1a  8457  pinn  8518  0nnq  8564  elpqn  8565  recn  8843  rexr  8893  ltord1  9315  leord1  9316  eqord1  9317  nnre  9769  nncn  9770  nnind  9780  nnnn0  9988  nn0re  9990  nn0cn  9991  nnz  10061  nn0z  10062  ublbneg  10318  nnq  10345  qcn  10346  rpre  10376  difreicc  10783  iccshftri  10786  iccshftli  10788  iccdili  10790  icccntri  10792  fzval2  10801  fzelp1  10854  expcllem  11130  expcl2lem  11131  m1expcl2  11141  bcm1k  11343  bcpasc  11349  hashbclem  11406  seqshft  11596  sqrlem5  11748  cau3lem  11854  caubnd  11858  climconst2  12038  rlimres  12048  lo1res  12049  lo1resb  12054  rlimresb  12055  o1resb  12056  rlimrege0  12069  o1of2  12102  o1rlimmul  12108  caurcvg  12165  caucvg  12167  zsum  12207  ackbijnn  12302  binomlem  12303  incexclem  12311  divalglem8  12615  sadadd  12674  smueqlem  12697  smumul  12700  isprm3  12783  phimullem  12863  prmdiveq  12870  unbenlem  12971  prmreclem2  12980  prmrec  12985  vdwnnlem1  13058  vdwnnlem3  13060  ramtcl2  13074  isstruct2  13173  structcnvcnv  13175  strlemor1  13251  imasdsval2  13435  xpsfrnel2  13483  mreunirn  13519  mrcfval  13526  mrisval  13548  isacs2  13571  acsfn  13577  homarcl  13876  arwval  13891  coafval  13912  coapm  13919  isdrs2  14089  isacs3lem  14285  psssdm2  14340  tsrss  14348  submnd0  14418  nmzsubg  14674  nmznsg  14677  resscntz  14823  cntzmhm  14830  odcl  14867  odlem2  14870  gexcl  14907  gexlem2  14909  gexdvds  14911  pgpssslw  14941  efginvrel2  15052  efginvrel1  15053  efgsp1  15062  efgsres  15063  efgsfo  15064  frgpinv  15089  frgpupf  15098  frgpup1  15100  subcmn  15149  torsubg  15162  dprd2dlem1  15292  dpjidcl  15309  ablfaclem3  15338  subrgpropd  15595  lssacs  15740  sralmod  15955  psrbaglefi  16134  resspsrmul  16177  mplsubglem  16195  ressmpladd  16217  ressmplmul  16218  ressmplvsca  16219  mplmonmul  16224  mplind  16259  ply1bascl  16300  psropprmul  16332  coe1mul2  16362  cnsubdrglem  16438  rege0subm  16444  zrngunit  16454  znrrg  16535  basdif0  16707  tgval2  16710  mreclatdemo  16849  ordtbas  16938  ordtrest  16948  ordtrestixx  16968  fincmp  17136  cmpfi  17151  iuncon  17170  1stcrest  17195  hauslly  17234  kgentop  17253  ptbasin  17288  ptcnplem  17331  txkgen  17362  infil  17574  filunirn  17593  uzrest  17608  elflim  17682  hauspwpwf1  17698  flffval  17700  fclsval  17719  isfcls  17720  fcfval  17744  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem3  17764  xmetunirn  17918  blfval  17963  blbas  17992  blres  17993  mopnval  18000  setsmstopn  18040  tmsval  18043  tngtopn  18182  qtopbaslem  18283  xrtgioo  18328  reperflem  18339  icccmplem1  18343  reconnlem2  18348  xrge0tsms  18355  icopnfhmeo  18457  icccvx  18464  bndth  18472  reparphti  18511  pcofval  18524  pcoval1  18527  pcoval2  18530  pcoass  18538  pcorevlem  18540  pcorev2  18542  pi1xfrcnv  18571  nmhmcn  18617  csscld  18692  cfilfval  18706  caufval  18717  cfilres  18738  bcthlem1  18762  ivthlem1  18827  ivthlem3  18829  ovolicc2lem3  18894  ovolicc2lem4  18895  ioombl1lem4  18934  vitalilem1  18979  mbflimsup  19037  i1fima2  19050  i1fd  19052  i1f0  19058  i1f1  19061  itg1addlem4  19070  itg1addlem5  19071  itg2cnlem2  19133  iblmbf  19138  ellimc2  19243  limcres  19252  limcun  19261  dvbsss  19268  perfdvf  19269  dvres2lem  19276  dvaddbr  19303  dvmulbr  19304  rolle  19353  cmvth  19354  dvlip  19356  dvlipcn  19357  dvle  19370  lhop1lem  19376  dvfsumle  19384  dvfsumge  19385  dvfsumabs  19386  dvfsumlem2  19390  ftc2  19407  itgparts  19410  itgsubstlem  19411  itgsubst  19412  mdegmullem  19480  deg1mul3  19517  coeval  19621  coeeu  19623  dgrval  19626  coef3  19630  coemulc  19652  dgrsub  19669  coecj  19675  dvply2  19682  dvnply  19684  quotval  19688  fta1  19704  plyexmo  19709  aacjcl  19723  taylfval  19754  dvtaylp  19765  abelth  19833  pilem2  19844  pilem3  19845  sinord  19912  recosf1o  19913  resinf1o  19914  tanord1  19915  eff1olem  19926  dvloglem  20011  dvlog  20014  dvlog2lem  20015  advlogexp  20018  logtayl  20023  logtayl2  20025  cxpcn3lem  20103  cxpcn3  20104  sqrcn  20106  loglesqr  20114  1cubr  20154  acosrecl  20215  rlimcnp2  20277  xrlimcnp  20279  efrlim  20280  jensen  20299  basellem4  20337  0sgm  20398  sgmf  20399  sgmnncl  20401  ppiprm  20405  chtprm  20407  prmorcht  20432  dvdsflip  20438  fsumdvdscom  20441  dvdsppwf1o  20442  musum  20447  musumsum  20448  muinv  20449  sgmppw  20452  chpchtsum  20474  dchrinvcl  20508  dchrghm  20511  dchrinv  20516  dchrsum2  20523  dchrsum  20524  rplogsumlem2  20650  rpvmasumlem  20652  dchrmusum2  20659  dchrvmasumlem1  20660  dchrvmasum2lem  20661  dchrisum0fmul  20671  dchrisum0ff  20672  dchrisum0flblem1  20673  dchrisum0re  20678  dchrisum0lem2a  20682  dchrisum0  20685  dirith2  20693  logsqvma  20707  pnt  20779  issubgoi  20993  opidon  21005  flddivrng  21098  rngosn3  21109  vcoprnelem  21150  nvvcop  21166  nvex  21183  phnv  21408  sheli  21809  cheli  21828  choc1  21922  shintcli  21924  chintcli  21926  shsleji  21965  pjini  22294  mayete3i  22323  mayete3iOLD  22324  dmadjop  22484  nlelshi  22656  cnlnadjeui  22673  cnlnssadj  22676  bdopadj  22678  pjimai  22772  stcl  22812  atelch  22940  ballotlemfp1  23066  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemfmpn  23069  ballotlemsup  23079  ballotlemfrceq  23103  ballotlemirc  23106  eliccioo  23131  partfun  23255  elfzo1  23294  rmulccn  23316  xrsmulgzz  23322  xrge0mulgnn0  23328  xrge0iifcnv  23330  xrge0iifcv  23331  xrge0iifiso  23332  xrge0iifhom  23334  xrge0npcan  23348  disjin  23377  iundisj2fi  23379  xrge0tsmsd  23397  rnlogblem  23416  esumval  23440  esumel  23441  esumcst  23451  issgon  23499  elrnsiga  23502  measvunilem  23555  imambfm  23582  br2base  23589  probmeasb  23648  subfacp1lem5  23730  cvmsi  23811  dedekindle  24098  zprod  24160  dfon2lem4  24213  wfrlem4  24330  wfrlem10  24336  frrlem4  24355  pprodss4v  24495  axlowdimlem5  24646  axlowdimlem6  24647  axlowdimlem7  24648  axlowdimlem15  24656  axlowdimlem16  24657  axlowdimlem17  24658  axlowdim  24661  axeuclidlem  24662  axcontlem2  24665  axcontlem7  24670  axcontlem8  24671  linedegen  24838  bpolydiflem  24861  bpoly4  24866  nnssi2  24966  nnssi3  24967  itg2addnc  25005  itg2gt0cn  25006  ftc1cnnc  25025  domintrefb  25166  mappow  25192  fvsnn  25217  elixp2b  25257  dstr  25274  posispre  25344  inposet  25381  reacomsmgrp1  25446  reacomsmgrp2  25447  reacomsmgrp3  25448  reacomsmgrp4  25449  clfsebsr  25452  resgcom  25454  basexre  25625  intopcoaconb  25643  iintlem2  25714  negveudr  25772  subclrvd  25777  issubcata  25949  inttaror  26003  smbkle  26146  pgapspf2  26156  ivthALT  26361  neibastop2lem  26412  cover2  26461  opelopab3  26476  sstotbnd2  26601  heibor1lem  26636  heiborlem10  26647  exidcl  26669  elrfi  26872  elrfirn  26873  elrfirn2  26874  mrefg3  26886  diophin  26955  diophun  26956  eq0rabdioph  26959  eqrabdioph  26960  rencldnfilem  27006  irrapx1  27016  pellex  27023  rmxycomplete  27105  rmxypos  27137  ltrmynn0  27138  jm2.23  27192  aomclem2  27255  fglmod  27274  lsmfgcl  27275  lmhmfgima  27285  lmhmfgsplit  27287  frlmsslsp  27351  isnumbasabl  27374  islinds4  27408  lmimlbs  27409  lbslcic  27414  dgrsub2  27442  itgocn  27472  symgtrinv  27516  psgnpmtr  27536  psgnghm  27540  acsfn1p  27610  phisum  27621  itgsin0pilem1  27847  itgsinexplem1  27851  itgsinexp  27852  stoweidlem15  27867  stoweidlem34  27886  stoweidlem51  27903  wallispilem2  27918  wallispi  27922  stirlinglem11  27936  4fvwrd4  28220  trlonprop  28341  onfrALTlem2  28610  onfrALTlem2VD  28981  bnj1533  29200  bnj110  29206  bnj1137  29341  bnj1286  29365  bnj1408  29382  bnj1417  29387  toycom  29784  osumcllem7N  30773  pexmidlem4N  30784  diaintclN  31870  dibintclN  31979  mapd1o  32460  hdmapevec  32650
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator