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

Theorem sseldi 3310
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 3308 . 2  |-  ( C  e.  A  ->  C  e.  B )
41, 3syl 16 1  |-  ( ph  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721    C_ wss 3284
This theorem is referenced by:  onfr  4584  sofld  5281  fvrn0  5716  elmpt2cl  6251  ofrval  6278  mpt2xopn0yelv  6427  mpt2xopxnop0  6429  tpostpos  6462  opiota  6498  riotacl  6527  riotasbc  6528  smores  6577  tz7.44-2  6628  omopthlem2  6862  f1opwfi  7372  supub  7424  suplub  7425  ordtypelem3  7449  ordtypelem4  7450  ordtypelem6  7452  ordtypelem7  7453  wemapso2lem  7479  wemapso2  7481  unxpwdom2  7516  cantnfres  7593  wemapwe  7614  oef1o  7615  cnfcomlem  7616  r1pwss  7670  r1elwf  7682  rankr1ai  7684  r0weon  7854  infxpenlem  7855  acnlem  7889  acndom2  7895  infpwfien  7903  alephfp  7949  ackbij1b  8079  cflim2  8103  fin23lem26  8165  isf32lem5  8197  isf32lem7  8199  isf32lem8  8200  isf32lem9  8201  isfin1-3  8226  fin1a2lem9  8248  fin1a2lem11  8250  hsmexlem5  8270  zorn2lem3  8338  zorn2lem4  8339  zorn2lem5  8340  ttukeylem6  8354  ttukeylem7  8355  iundom2g  8375  fpwwe2lem12  8476  pwfseqlem3  8495  gch2  8514  wunom  8555  rexrd  9094  nnred  9975  nncnd  9976  un0addcl  10213  un0mulcl  10214  nnnn0d  10234  nn0red  10235  suprzcl  10309  nn0zd  10333  zred  10335  zsupss  10525  rpnnen1lem1  10560  rpnnen1lem2  10561  rpred  10608  fzfi  11270  seqf1olem1  11321  expcl2lem  11352  m1expcl  11363  hashxrcl  11599  seqcoll2  11672  wrdeqcats1  11747  wrdind  11750  limsupgre  12234  rlimpm  12253  rlimclim  12299  isercolllem1  12417  isercolllem2  12418  isercoll  12420  iseraltlem2  12435  iseraltlem3  12436  fsumcvg3  12482  ackbijnn  12566  bitsval  12895  bitsfzolem  12905  bitsinv1  12913  smuval2  12953  gcdcllem3  12972  eulerthlem2  13130  prmdivdiv  13135  prmreclem1  13243  prmreclem2  13244  prmreclem3  13245  1arith  13254  4sqlem13  13284  4sqlem14  13285  4sqlem17  13288  vdwlem5  13312  vdwlem8  13315  vdwlem12  13319  vdwnnlem3  13324  ramtlecl  13327  ramcl2lem  13336  ramcl2  13343  ramxrcl  13344  submrc  13812  mreexexlem2d  13829  catlid  13867  catrid  13868  sscpwex  13974  subcrcl  13975  sscres  13982  wunfunc  14055  funcres2c  14057  cofull  14090  cofth  14091  coffth  14092  rescfth  14093  homarel  14150  arwrcl  14158  idaf  14177  homdmcoa  14181  coaval  14182  coapm  14185  catciso  14221  catcoppccl  14222  catcfuccl  14223  catcxpccl  14263  acsfiindd  14562  psssdm2  14606  submrcl  14706  gsumval2  14742  issubg  14903  isnsg  14928  nmzsubg  14940  conjnmz  14998  conjnmzb  14999  cntzsubm  15093  cntzsubg  15094  odlem2  15136  gexlem2  15175  sylow1lem2  15192  sylow1lem4  15194  sylow2a  15212  efglem  15307  efgtf  15313  efgtlen  15317  efgsres  15329  efgsfo  15330  efgredlemg  15333  efgredleme  15334  efgredlemd  15335  efgredlemc  15336  efgredlem  15338  efgred  15339  efgcpbllemb  15346  frgpuplem  15363  frgpnabllem2  15444  cyggex2  15465  dprdfsub  15538  dprdf11  15540  dprd2da  15559  ablfac2  15606  issubrg  15827  cntzsubr  15859  abvrcl  15868  lbsextlem3  16191  sralmod  16217  rrgeq0  16309  psrbagconf1o  16398  psrass1lem  16401  psrdi  16429  psrdir  16430  psrass23  16432  resspsrmul  16439  mplelf  16456  mplsubrglem  16461  mpladd  16464  mplmul  16465  mplvsca  16469  mplmonmul  16486  mplcoe2  16489  mplind  16521  psropprmul  16591  zlpirlem2  16728  zlpirlem3  16729  znf1o  16791  cygznlem2a  16807  ocvlss  16858  lsmcss  16878  isobs  16906  neiptoptop  17154  restbas  17180  ordtbas2  17213  ordtopn1  17216  ordtopn2  17217  ordtrest  17224  iocpnfordt  17237  icomnfordt  17238  lmrcl  17253  subbascn  17276  lmss  17320  cnconn  17442  clscon  17450  concompclo  17455  subislly  17501  cldllycmp  17515  kgeni  17526  llycmpkgen2  17539  1stckgenlem  17542  ptbasfi  17570  xkoopn  17578  txcls  17593  dfac14lem  17606  txcnp  17609  ptcnplem  17610  upxp  17612  txtube  17629  txcmplem1  17630  txcmplem2  17631  txkgen  17641  xkopt  17644  xkococnlem  17648  txcon  17678  basqtop  17700  tgqtop  17701  kqnrmlem1  17732  kqnrmlem2  17733  nrmhmph  17783  ptcmpfi  17802  elmptrab  17816  uzrest  17886  fclsfnflim  18016  flimfnfcls  18017  cnpfcf  18030  alexsubALTlem3  18037  alexsubALTlem4  18038  ptcmplem2  18041  ptcmplem5  18044  tsmsres  18130  restutop  18224  prdsxmetlem  18355  isxms2  18435  prdsbl  18478  met2ndci  18509  nmdvr  18663  nrginvrcnlem  18683  nrginvrcn  18684  tgqioo  18788  zdis  18804  reperflem  18806  reconnlem2  18815  reconn  18816  xrge0gsumle  18821  xrge0tsms  18822  xmetdcn  18826  metdcn  18828  metdscn2  18844  cncfmpt2ss  18902  icchmeo  18923  iccpnfcnv  18926  xrhmeo  18928  icccvx  18932  cnheibor  18937  bndth  18940  evth  18941  lebnum  18946  isphtpc  18976  reparphti  18979  pcoass  19006  nmoleub2lem  19079  nmoleub2lem3  19080  nmoleub2lem2  19081  nmoleub3  19084  nmhmcn  19085  cfili  19178  cfilfcls  19184  caussi  19207  equivcau  19210  minveclem4b  19289  minveclem4  19290  evthicc2  19314  ovolfcl  19320  ovolfioo  19321  ovolficc  19322  ovolficcss  19323  ovolfsval  19324  ovolmge0  19330  ovollb2lem  19341  ovolunlem1a  19349  ovoliunlem1  19355  ovolicc1  19369  ovolicc2lem4  19373  ovolicc2lem5  19374  ioombl1lem2  19410  ioombl1lem4  19412  ovolfs2  19420  ioorcl  19426  uniiccdif  19427  uniioovol  19428  uniiccvol  19429  uniioombllem2a  19431  uniioombllem2  19432  uniioombllem3a  19433  uniioombllem3  19434  uniioombllem4  19435  uniioombllem5  19436  uniioombllem6  19437  dyadmbl  19449  volsup2  19454  volivth  19456  vitalilem1  19457  vitalilem2  19458  vitalilem4  19460  mbfimaopnlem  19504  cncombf  19507  cnmbf  19508  mbflimsup  19515  mbfi1fseqlem3  19566  mbfi1fseqlem4  19567  mbfi1fseqlem5  19568  itg2const2  19590  itg2lea  19593  itg2eqa  19594  itg2split  19598  itg2i1fseq  19604  itg2gt0  19609  limcco  19737  dvcl  19743  perfdvf  19747  dvreslem  19753  dvres2lem  19754  dvidlem  19759  dvcnp2  19763  dvmulbr  19782  dvferm1lem  19825  dvferm2lem  19827  dvferm  19829  rolle  19831  dvlipcn  19835  dvlip2  19836  c1liplem1  19837  c1lip2  19839  dvgt0lem1  19843  dvivthlem1  19849  dvivth  19851  lhop1lem  19854  lhop1  19855  lhop2  19856  lhop  19857  dvfsumlem1  19867  dvfsumlem2  19868  dvfsumlem3  19869  dvfsumlem4  19870  dvfsumrlimge0  19871  dvfsumrlim  19872  dvfsumrlim2  19873  dvfsum2  19875  ftc1lem5  19881  ftc1lem6  19882  itgsubstlem  19889  itgsubst  19890  mdegleb  19944  mdegaddle  19954  mdegvsca  19956  mdegmullem  19958  ig1peu  20051  plybss  20070  plyaddcl  20096  plymulcl  20097  plysubcl  20098  coeidlem  20113  coesub  20132  dgrmulc  20146  dgrcolem1  20148  dgrcolem2  20149  dgrco  20150  quotlem  20174  quotcl2  20176  quotdgr  20177  plyrem  20179  facth  20180  quotcan  20183  vieta1lem1  20184  vieta1  20186  elqaalem3  20195  aalioulem2  20207  aalioulem3  20208  taylfvallem1  20230  tayl0  20235  dvntaylp  20244  taylthlem1  20246  taylthlem2  20247  radcnvlt1  20291  radcnvle  20293  pserulm  20295  psercnlem2  20297  psercnlem1  20298  psercn  20299  pserdvlem1  20300  pserdvlem2  20301  abelthlem3  20306  abelthlem5  20308  abelthlem6  20309  abelth  20314  efcvx  20322  tanord  20397  tanregt0  20398  efif1olem4  20404  logtayl  20508  logccv  20511  cxpcn3  20589  ssscongptld  20623  chordthmlem  20630  chordthmlem4  20633  chordthmlem5  20634  chordthm  20635  asinrecl  20699  atantan  20720  dvatan  20732  leibpi  20739  rlimcnp  20761  efrlim  20765  cvxcl  20780  scvxcvx  20781  jensenlem1  20782  jensenlem2  20783  jensen  20784  amgmlem  20785  harmonicbnd3  20803  wilthlem1  20808  ftalem3  20814  ftalem5  20816  ftalem7  20818  basellem3  20822  basellem4  20823  basellem5  20824  ppisval  20843  chtf  20848  efchtcl  20851  chtge0  20852  sgmval2  20883  ppinprm  20892  chtprm  20893  chtnprm  20894  chtwordi  20896  chtdif  20898  efchtdvds  20899  sqff1o  20922  fsumdvdsdiaglem  20925  fsumdvdsdiag  20926  fsumdvdscom  20927  musum  20933  muinv  20935  dvdsmulf1o  20936  sgmmul  20942  chtlepsi  20947  chtleppi  20951  pclogsum  20956  chpval2  20959  chpchtsum  20960  chpub  20961  perfectlem2  20971  dchrelbasd  20980  dchrrcl  20981  dchrzrh1  20985  dchrzrhmul  20987  dchrinvcl  20994  dchrfi  20996  dchrghm  20997  dchr1  20998  dchrabs  21001  dchrinv  21002  dchrptlem2  21006  dchrsum2  21009  sumdchr2  21011  sum2dchr  21015  lgscl  21051  lgsquadlem1  21095  lgsquadlem2  21096  2sqlem6  21110  2sqlem8  21113  2sqlem9  21114  chebbnd1lem1  21120  chtppilimlem1  21124  rplogsumlem2  21136  dchrisum0flblem1  21159  rpvmasum2  21163  dchrisum0re  21164  dchrisum0lema  21165  dchrisum0lem1b  21166  dchrisum0lem1  21167  dchrisum0lem2a  21168  dchrisum0lem2  21169  dchrisum0lem3  21170  dchrisum0  21171  rplogsum  21178  dirith2  21179  mudivsum  21181  mulogsum  21183  mulog2sumlem2  21186  vmalogdivsum2  21189  logsqvma  21193  logsqvma2  21194  selberglem3  21198  selberg  21199  chpdifbndlem1  21204  selberg34r  21222  pntsval2  21227  pntrlog2bndlem1  21228  pntpbnd1a  21236  pntpbnd1  21237  pntpbnd2  21238  pntibndlem2a  21241  pntibndlem2  21242  pntibndlem3  21243  pntlemd  21245  padicabv  21281  umgrass  21311  umgran0  21312  usgrass  21341  redwlk  21563  issubgo  21848  nvvop  22045  nmcnc  22149  ubthlem1  22329  minvecolem2  22334  minvecolem3  22335  minvecolem5  22340  minvecolem6  22341  minvecolem7  22342  hlimcaui  22696  pjocini  23157  eliccelico  24097  elicoelioo  24098  iundisjfi  24109  iundisj2fi  24110  divnumden2  24118  xrsmulgzz  24157  ressmulgnn  24162  ressmulgnn0  24163  xrge0addass  24168  xrge0addgt0  24171  xrge0adddir  24172  xrge0npcan  24173  fsumrp0cl  24174  xrge0tsmsd  24180  dvrdir  24183  rdivmuldivd  24184  dvrcan5  24186  elrhmunit  24215  rhmunitinv  24217  cnre2csqima  24266  tpr2rico  24267  cnvordtrestixx  24268  xrge0iifcnv  24276  xrge0iifhom  24280  xrge0mulc1cn  24284  rge0scvg  24292  lmxrge0  24294  cnzh  24311  rezh  24312  qqhval2  24323  qqhvq  24328  qqhnm  24331  qqhcn  24332  qqhucn  24333  indsum  24377  indf1ofs  24380  esumel  24399  esumle  24406  esummono  24407  gsumesum  24408  esumlub  24409  esumlef  24411  esumcst  24412  esumfzf  24416  esumfsup  24417  esumfsupre  24418  esumpinfval  24420  esumpfinvallem  24421  esumpfinval  24422  esumpfinvalf  24423  esumpinfsum  24424  esumpcvgval  24425  esumpmono  24426  esummulc1  24428  esummulc2  24429  esumdivc  24430  hasheuni  24432  esumcvg  24433  sigainb  24476  measun  24522  measunl  24527  measiun  24529  meascnbl  24530  voliune  24542  volfiniune  24543  dya2icoseg2  24585  dya2iocnrect  24588  sxbrsigalem2  24593  sibfof  24611  probun  24634  probdif  24635  probvalrnd  24639  probmeasb  24645  cndprobin  24649  bayesth  24654  ballotlemsdom  24726  ballotlemrv2  24736  ballotlemfrci  24742  lgamgulmlem2  24771  lgamcvg2  24796  subfacp1lem5  24827  erdszelem4  24837  erdszelem6  24839  erdszelem7  24840  erdszelem8  24841  erdszelem9  24842  conpcon  24879  cvxscon  24887  rescon  24890  iccllyscon  24894  rellyscon  24895  cvmsrcl  24908  cvmliftmolem2  24926  cvmlift2lem12  24958  cvmlift3  24972  snmlval  24975  clim2prod  25173  ntrivcvg  25182  ntrivcvgfvn0  25184  ntrivcvgtail  25185  ntrivcvgmullem  25186  ntrivcvgmul  25187  prodrblem  25212  prodmolem2a  25217  axlowdimlem16  25804  axcontlem10  25820  mblfinlem  26147  itg2addnclem3  26161  itg2addnc  26162  itg2gt0cn  26163  ftc1cnnclem  26181  islocfin  26270  neibastop1  26282  fdc  26343  prdsbnd  26396  ismtyval  26403  heiborlem3  26416  heiborlem5  26418  heiborlem10  26423  rrnequiv  26438  eldiophb  26709  4rexfrabdioph  26752  6rexfrabdioph  26753  diophren  26768  rencldnfilem  26775  pellexlem3  26788  pellfundglb  26842  rmxypairf1o  26868  rmxycomplete  26874  rmxyneg  26877  rmxyadd  26878  rmxy1  26879  rmxy0  26880  monotuz  26898  jm2.22  26960  aomclem2  27024  isnumbasgrp  27144  dfacbasgrp  27145  hbtlem2  27200  hbt  27206  elmnc  27213  symggen  27283  symgtrinv  27285  psgnunilem5  27289  psgnunilem2  27290  psgnuni  27294  issdrg  27377  cntzsdrg  27382  mon1psubm  27397  stoweidlem26  27646  stoweidlem51  27671  suctrALT3  28749  chordthmALT  28759  bnj1213  28880  bnj1417  29120  osumcllem7N  30448  pexmidlem4N  30459
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 2389
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 2395  df-cleq 2401  df-clel 2404  df-in 3291  df-ss 3298
  Copyright terms: Public domain W3C validator