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

Theorem sseldi 3191
Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
Hypotheses
Ref Expression
sseli.1  |-  A  C_  B
sseldi.2  |-  ( ph  ->  C  e.  A )
Assertion
Ref Expression
sseldi  |-  ( ph  ->  C  e.  B )

Proof of Theorem sseldi
StepHypRef Expression
1 sseldi.2 . 2  |-  ( ph  ->  C  e.  A )
2 sseli.1 . . 3  |-  A  C_  B
32sseli 3189 . 2  |-  ( C  e.  A  ->  C  e.  B )
41, 3syl 15 1  |-  ( ph  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696    C_ wss 3165
This theorem is referenced by:  onfr  4447  sofld  5137  fvrn0  5566  elmpt2cl  6077  ofrval  6104  tpostpos  6270  opiota  6306  riotacl  6335  riotasbc  6336  smores  6385  tz7.44-2  6436  omopthlem2  6670  f1opwfi  7175  supub  7226  suplub  7227  ordtypelem3  7251  ordtypelem4  7252  ordtypelem6  7254  ordtypelem7  7255  wemapso2lem  7281  wemapso2  7283  unxpwdom2  7318  cantnfres  7395  wemapwe  7416  oef1o  7417  cnfcomlem  7418  r1pwss  7472  r1elwf  7484  rankr1ai  7486  r0weon  7656  infxpenlem  7657  acnlem  7691  acndom2  7697  infpwfien  7705  alephfp  7751  ackbij1lem18  7879  ackbij1b  7881  cflim2  7905  fin23lem26  7967  fin23lem30  7984  isf32lem5  7999  isf32lem7  8001  isf32lem8  8002  isf32lem9  8003  isfin1-3  8028  fin1a2lem9  8050  fin1a2lem11  8052  hsmexlem5  8072  zorn2lem3  8141  zorn2lem4  8142  zorn2lem5  8143  ttukeylem6  8157  ttukeylem7  8158  iundom2g  8178  fpwwe2lem12  8279  pwfseqlem3  8298  gch2  8317  wunom  8358  rexrd  8897  nnred  9777  nncnd  9778  un0addcl  10013  un0mulcl  10014  nnnn0d  10034  nn0red  10035  suprzcl  10107  nn0zd  10131  zred  10133  zsupss  10323  rpnnen1lem1  10358  rpnnen1lem2  10359  rpred  10406  fzfi  11050  seqf1olem1  11101  expcl2lem  11131  m1expcl  11142  hashxrcl  11367  seqcoll2  11418  wrdeqcats1  11490  wrdind  11493  limsupgre  11971  rlimpm  11990  rlimclim  12036  isercolllem1  12154  isercolllem2  12155  isercoll  12157  iseraltlem2  12171  iseraltlem3  12172  fsumcvg3  12218  ackbijnn  12302  bitsval  12631  bitsfzolem  12641  bitsinv1  12649  smuval2  12689  gcdcllem3  12708  eulerthlem2  12866  prmdivdiv  12871  prmreclem1  12979  prmreclem2  12980  prmreclem3  12981  1arith  12990  4sqlem13  13020  4sqlem14  13021  4sqlem17  13024  vdwlem5  13048  vdwlem8  13051  vdwlem12  13055  vdwnnlem3  13060  ramtlecl  13063  ramcl2lem  13072  ramcl2  13079  ramxrcl  13080  submrc  13546  mreexexlem2d  13563  catlid  13601  catrid  13602  sscpwex  13708  subcrcl  13709  sscres  13716  wunfunc  13789  funcres2c  13791  cofull  13824  cofth  13825  coffth  13826  rescfth  13827  homarel  13884  arwrcl  13892  idaf  13911  homdmcoa  13915  coaval  13916  coapm  13919  catciso  13955  catcoppccl  13956  catcfuccl  13957  catcxpccl  13997  acsfiindd  14296  psssdm2  14340  submrcl  14440  gsumval2  14476  issubg  14637  isnsg  14662  nmzsubg  14674  conjnmz  14732  conjnmzb  14733  cntzsubm  14827  cntzsubg  14828  odlem2  14870  gexlem2  14909  sylow1lem2  14926  sylow1lem4  14928  sylow2a  14946  efglem  15041  efgtf  15047  efgtlen  15051  efgsres  15063  efgsfo  15064  efgredlemg  15067  efgredleme  15068  efgredlemd  15069  efgredlemc  15070  efgredlem  15072  efgred  15073  efgcpbllemb  15080  frgpuplem  15097  frgpnabllem2  15178  cyggex2  15199  dprdfsub  15272  dprdf11  15274  dprd2da  15293  ablfac2  15340  isdrng2  15538  issubrg  15561  cntzsubr  15593  abvrcl  15602  lsppratlem1  15916  lsppratlem2  15917  lbsextlem3  15929  sralmod  15955  rrgeq0  16047  psrbagconf1o  16136  psrass1lem  16139  psrdi  16167  psrdir  16168  psrass23  16170  resspsrmul  16177  mplelf  16194  mplsubrglem  16199  mpladd  16202  mplmul  16203  mplvsca  16207  mplmonmul  16224  mplcoe2  16227  mplind  16259  psropprmul  16332  zlpirlem2  16458  zlpirlem3  16459  znf1o  16521  cygznlem2a  16537  ocvlss  16588  lsmcss  16608  isobs  16636  restbas  16905  ordtbas2  16937  ordtopn1  16940  ordtopn2  16941  ordtrest  16948  iocpnfordt  16961  icomnfordt  16962  lmrcl  16977  subbascn  17000  lmss  17042  hauscmplem  17149  cnconn  17164  clscon  17172  concompclo  17177  subislly  17223  cldllycmp  17237  kgeni  17248  llycmpkgen2  17261  1stckgenlem  17264  ptbasfi  17292  xkoopn  17300  txcls  17315  dfac14lem  17327  txcnp  17330  ptcnplem  17331  upxp  17333  txtube  17350  txcmplem1  17351  txcmplem2  17352  txkgen  17362  xkopt  17365  xkococnlem  17369  txcon  17399  basqtop  17418  tgqtop  17419  kqnrmlem1  17450  kqnrmlem2  17451  nrmhmph  17501  ptcmpfi  17520  elmptrab  17538  uzrest  17608  fclsfnflim  17738  flimfnfcls  17739  cnpfcf  17752  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem2  17763  ptcmplem5  17766  tsmsres  17842  prdsxmetlem  17948  imasdsf1olem  17953  isxms2  18010  prdsbl  18053  met2ndci  18084  nmdvr  18197  nrginvrcnlem  18217  nrginvrcn  18218  tgqioo  18322  zdis  18338  reperflem  18339  reconnlem2  18348  reconn  18349  xrge0gsumle  18354  xrge0tsms  18355  xmetdcn  18359  metdcn  18361  metdscn2  18377  cncfmpt2ss  18435  icchmeo  18455  iccpnfcnv  18458  xrhmeo  18460  icccvx  18464  cnheibor  18469  bndth  18472  evth  18473  lebnum  18478  isphtpc  18508  reparphti  18511  pcoass  18538  nmoleub2lem  18611  nmoleub2lem3  18612  nmoleub2lem2  18613  nmoleub3  18616  nmhmcn  18617  cfili  18710  cfilfcls  18716  caussi  18739  equivcau  18742  minveclem4b  18811  minveclem4  18812  evthicc2  18836  ovolfcl  18842  ovolfioo  18843  ovolficc  18844  ovolficcss  18845  ovolfsval  18846  ovolmge0  18852  ovollb2lem  18863  ovolunlem1a  18871  ovoliunlem1  18877  ovolicc1  18891  ovolicc2lem4  18895  ovolicc2lem5  18896  ioombl1lem2  18932  ioombl1lem4  18934  ovolfs2  18942  ioorcl  18948  uniiccdif  18949  uniioovol  18950  uniiccvol  18951  uniioombllem2a  18953  uniioombllem2  18954  uniioombllem3a  18955  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  uniioombllem6  18959  dyadmbl  18971  volsup2  18976  volivth  18978  vitalilem1  18979  vitalilem2  18980  vitalilem4  18982  mbfimaopnlem  19026  cncombf  19029  cnmbf  19030  mbflimsup  19037  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  itg2const2  19112  itg2lea  19115  itg2eqa  19116  itg2split  19120  itg2i1fseq  19126  itg2gt0  19131  limcco  19259  dvcl  19265  perfdvf  19269  dvreslem  19275  dvres2lem  19276  dvidlem  19281  dvcnp2  19285  dvmulbr  19304  dvrec  19320  dvferm1lem  19347  dvferm2lem  19349  dvferm  19351  rolle  19353  dvlipcn  19357  dvlip2  19358  c1liplem1  19359  c1lip2  19361  dvgt0lem1  19365  dvivthlem1  19371  dvivth  19373  lhop1lem  19376  lhop1  19377  lhop2  19378  lhop  19379  dvfsumlem1  19389  dvfsumlem2  19390  dvfsumlem3  19391  dvfsumlem4  19392  dvfsumrlimge0  19393  dvfsumrlim  19394  dvfsumrlim2  19395  dvfsum2  19397  ftc1lem5  19403  ftc1lem6  19404  itgsubstlem  19411  itgsubst  19412  mdegleb  19466  mdegaddle  19476  mdegvsca  19478  mdegmullem  19480  ig1peu  19573  plybss  19592  plyaddcl  19618  plymulcl  19619  plysubcl  19620  coeidlem  19635  coesub  19654  dgrmulc  19668  dgrcolem1  19670  dgrcolem2  19671  dgrco  19672  quotlem  19696  quotcl2  19698  quotdgr  19699  plyrem  19701  facth  19702  quotcan  19705  vieta1lem1  19706  vieta1  19708  elqaalem3  19717  aalioulem2  19729  aalioulem3  19730  taylfvallem1  19752  tayl0  19757  dvntaylp  19766  taylthlem1  19768  taylthlem2  19769  radcnvlt1  19810  radcnvle  19812  pserulm  19814  psercnlem2  19816  psercnlem1  19817  psercn  19818  pserdvlem1  19819  pserdvlem2  19820  abelthlem3  19825  abelthlem5  19827  abelthlem6  19828  abelth  19833  efcvx  19841  tanord  19916  tanregt0  19917  efif1olem4  19923  logtayl  20023  logccv  20026  cxpcn3  20104  ssscongptld  20138  chordthmlem  20145  chordthmlem4  20148  chordthmlem5  20149  chordthm  20150  asinrecl  20214  atantan  20235  dvatan  20247  leibpi  20254  rlimcnp  20276  efrlim  20280  cvxcl  20295  scvxcvx  20296  jensenlem1  20297  jensenlem2  20298  jensen  20299  amgmlem  20300  harmonicbnd3  20317  wilthlem1  20322  ftalem3  20328  ftalem5  20330  ftalem7  20332  basellem3  20336  basellem4  20337  basellem5  20338  ppisval  20357  chtf  20362  efchtcl  20365  chtge0  20366  sgmval2  20397  ppinprm  20406  chtprm  20407  chtnprm  20408  chtwordi  20410  chtdif  20412  efchtdvds  20413  sqff1o  20436  fsumdvdsdiaglem  20439  fsumdvdsdiag  20440  fsumdvdscom  20441  musum  20447  muinv  20449  dvdsmulf1o  20450  sgmmul  20456  chtlepsi  20461  chtleppi  20465  pclogsum  20470  chpval2  20473  chpchtsum  20474  chpub  20475  perfectlem2  20485  dchrelbasd  20494  dchrrcl  20495  dchrzrh1  20499  dchrzrhmul  20501  dchrinvcl  20508  dchrfi  20510  dchrghm  20511  dchr1  20512  dchrabs  20515  dchrinv  20516  dchrptlem2  20520  dchrsum2  20523  sumdchr2  20525  sum2dchr  20529  lgscl  20565  lgsquadlem1  20609  lgsquadlem2  20610  2sqlem6  20624  2sqlem8  20627  2sqlem9  20628  chebbnd1lem1  20634  chtppilimlem1  20638  rplogsumlem2  20650  dchrisum0flblem1  20673  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lema  20679  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  dchrisum0lem3  20684  dchrisum0  20685  rplogsum  20692  dirith2  20693  mudivsum  20695  mulogsum  20697  mulog2sumlem2  20700  vmalogdivsum2  20703  logsqvma  20707  logsqvma2  20708  selberglem3  20712  selberg  20713  chpdifbndlem1  20718  selberg34r  20736  pntsval2  20741  pntrlog2bndlem1  20742  pntpbnd1a  20750  pntpbnd1  20751  pntpbnd2  20752  pntibndlem2a  20755  pntibndlem2  20756  pntibndlem3  20757  pntlemd  20759  padicabv  20795  issubgo  20986  nvvop  21181  nmcnc  21285  ubthlem1  21465  minvecolem2  21470  minvecolem3  21471  minvecolem5  21476  minvecolem6  21477  minvecolem7  21478  hlimcaui  21832  pjocini  22293  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemimin  23080  ballotlemsdom  23086  ballotlemrv2  23096  ballotlemfrci  23102  eliccelico  23285  elicoelioo  23286  ssnnssfz  23292  cnre2csqima  23310  tpr2rico  23311  cnvordtrestixx  23312  xrsmulgzz  23322  ressmulgnn  23323  ressmulgnn0  23324  xrge0iifcnv  23330  xrge0iifhom  23334  xrge0mulc1cn  23338  xrge0addass  23344  xrge0addgt0  23346  xrge0adddir  23347  fsumrp0cl  23349  iundisjfi  23378  iundisj2fi  23379  rge0scvg  23388  lmxrge0  23390  xrge0tsmsd  23397  esumle  23448  esumlef  23450  esumcst  23451  esumpinfval  23456  esumpfinvallem  23457  esumpfinval  23458  esumpfinvalf  23459  esumpinfsum  23460  esumpcvgval  23461  esumpmono  23462  esummulc1  23464  esummulc2  23465  esumdivc  23466  hasheuni  23468  esumcvg  23469  sigainb  23512  measxun  23554  measiun  23560  meascnbl  23561  indsum  23621  indf1ofs  23624  probun  23637  probdif  23638  probvalrnd  23642  cndprobin  23652  bayesth  23657  dstrvprob  23687  coinfliplem  23694  subfacp1lem5  23730  erdszelem4  23740  erdszelem6  23742  erdszelem7  23743  erdszelem8  23744  erdszelem9  23745  conpcon  23781  cvxscon  23789  rescon  23792  iccllyscon  23796  rellyscon  23797  cvmsrcl  23810  cvmliftmolem2  23828  cvmlift2lem12  23860  cvmlift3  23874  umgrass  23886  umgran0  23887  umgraex  23890  snmlval  23929  prodrblem  24152  prodmolem2a  24157  axlowdimlem16  24657  axcontlem10  24673  itg2gt0cn  25006  ftc1cnnclem  25024  inposet  25381  besubbeca  25951  pfsubkl  26150  islocfin  26399  neibastop1  26411  fdc  26558  prdsbnd  26620  ismtyval  26627  heiborlem3  26640  heiborlem5  26642  heiborlem10  26647  rrnequiv  26662  eldiophb  26939  4rexfrabdioph  26982  6rexfrabdioph  26983  diophren  26999  rencldnfilem  27006  pellexlem3  27019  pellfundglb  27073  rmxypairf1o  27099  rmxycomplete  27105  rmxyneg  27108  rmxyadd  27109  rmxy1  27110  rmxy0  27111  monotuz  27129  jm2.22  27191  aomclem2  27255  isnumbasgrp  27375  dfacbasgrp  27376  hbtlem2  27431  hbt  27437  elmnc  27444  pmtrfinv  27505  symggen  27514  symgtrinv  27516  psgnunilem5  27520  psgnunilem2  27521  psgnuni  27525  issdrg  27608  cntzsdrg  27613  mon1psubm  27628  wallispilem4  27920  mpt2xopn0yelv  28195  mpt2xopxnop0  28197  usgrass  28244  nbgrael  28275  redwlk  28364  suctrALT3  29016  chordthmALT  29026  bnj1213  29147  bnj1417  29387  osumcllem7N  30773  pexmidlem4N  30784
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