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

Theorem sseldi 3289
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 3287 . 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 1717    C_ wss 3263
This theorem is referenced by:  onfr  4561  sofld  5258  fvrn0  5693  elmpt2cl  6227  ofrval  6254  mpt2xopn0yelv  6400  mpt2xopxnop0  6402  tpostpos  6435  opiota  6471  riotacl  6500  riotasbc  6501  smores  6550  tz7.44-2  6601  omopthlem2  6835  f1opwfi  7345  supub  7397  suplub  7398  ordtypelem3  7422  ordtypelem4  7423  ordtypelem6  7425  ordtypelem7  7426  wemapso2lem  7452  wemapso2  7454  unxpwdom2  7489  cantnfres  7566  wemapwe  7587  oef1o  7588  cnfcomlem  7589  r1pwss  7643  r1elwf  7655  rankr1ai  7657  r0weon  7827  infxpenlem  7828  acnlem  7862  acndom2  7868  infpwfien  7876  alephfp  7922  ackbij1b  8052  cflim2  8076  fin23lem26  8138  isf32lem5  8170  isf32lem7  8172  isf32lem8  8173  isf32lem9  8174  isfin1-3  8199  fin1a2lem9  8221  fin1a2lem11  8223  hsmexlem5  8243  zorn2lem3  8311  zorn2lem4  8312  zorn2lem5  8313  ttukeylem6  8327  ttukeylem7  8328  iundom2g  8348  fpwwe2lem12  8449  pwfseqlem3  8468  gch2  8487  wunom  8528  rexrd  9067  nnred  9947  nncnd  9948  un0addcl  10185  un0mulcl  10186  nnnn0d  10206  nn0red  10207  suprzcl  10281  nn0zd  10305  zred  10307  zsupss  10497  rpnnen1lem1  10532  rpnnen1lem2  10533  rpred  10580  fzfi  11238  seqf1olem1  11289  expcl2lem  11320  m1expcl  11331  hashxrcl  11567  seqcoll2  11640  wrdeqcats1  11715  wrdind  11718  limsupgre  12202  rlimpm  12221  rlimclim  12267  isercolllem1  12385  isercolllem2  12386  isercoll  12388  iseraltlem2  12403  iseraltlem3  12404  fsumcvg3  12450  ackbijnn  12534  bitsval  12863  bitsfzolem  12873  bitsinv1  12881  smuval2  12921  gcdcllem3  12940  eulerthlem2  13098  prmdivdiv  13103  prmreclem1  13211  prmreclem2  13212  prmreclem3  13213  1arith  13222  4sqlem13  13252  4sqlem14  13253  4sqlem17  13256  vdwlem5  13280  vdwlem8  13283  vdwlem12  13287  vdwnnlem3  13292  ramtlecl  13295  ramcl2lem  13304  ramcl2  13311  ramxrcl  13312  submrc  13780  mreexexlem2d  13797  catlid  13835  catrid  13836  sscpwex  13942  subcrcl  13943  sscres  13950  wunfunc  14023  funcres2c  14025  cofull  14058  cofth  14059  coffth  14060  rescfth  14061  homarel  14118  arwrcl  14126  idaf  14145  homdmcoa  14149  coaval  14150  coapm  14153  catciso  14189  catcoppccl  14190  catcfuccl  14191  catcxpccl  14231  acsfiindd  14530  psssdm2  14574  submrcl  14674  gsumval2  14710  issubg  14871  isnsg  14896  nmzsubg  14908  conjnmz  14966  conjnmzb  14967  cntzsubm  15061  cntzsubg  15062  odlem2  15104  gexlem2  15143  sylow1lem2  15160  sylow1lem4  15162  sylow2a  15180  efglem  15275  efgtf  15281  efgtlen  15285  efgsres  15297  efgsfo  15298  efgredlemg  15301  efgredleme  15302  efgredlemd  15303  efgredlemc  15304  efgredlem  15306  efgred  15307  efgcpbllemb  15314  frgpuplem  15331  frgpnabllem2  15412  cyggex2  15433  dprdfsub  15506  dprdf11  15508  dprd2da  15527  ablfac2  15574  issubrg  15795  cntzsubr  15827  abvrcl  15836  lbsextlem3  16159  sralmod  16185  rrgeq0  16277  psrbagconf1o  16366  psrass1lem  16369  psrdi  16397  psrdir  16398  psrass23  16400  resspsrmul  16407  mplelf  16424  mplsubrglem  16429  mpladd  16432  mplmul  16433  mplvsca  16437  mplmonmul  16454  mplcoe2  16457  mplind  16489  psropprmul  16559  zlpirlem2  16692  zlpirlem3  16693  znf1o  16755  cygznlem2a  16771  ocvlss  16822  lsmcss  16842  isobs  16870  neiptoptop  17118  restbas  17144  ordtbas2  17177  ordtopn1  17180  ordtopn2  17181  ordtrest  17188  iocpnfordt  17201  icomnfordt  17202  lmrcl  17217  subbascn  17240  lmss  17284  cnconn  17406  clscon  17414  concompclo  17419  subislly  17465  cldllycmp  17479  kgeni  17490  llycmpkgen2  17503  1stckgenlem  17506  ptbasfi  17534  xkoopn  17542  txcls  17557  dfac14lem  17570  txcnp  17573  ptcnplem  17574  upxp  17576  txtube  17593  txcmplem1  17594  txcmplem2  17595  txkgen  17605  xkopt  17608  xkococnlem  17612  txcon  17642  basqtop  17664  tgqtop  17665  kqnrmlem1  17696  kqnrmlem2  17697  nrmhmph  17747  ptcmpfi  17766  elmptrab  17780  uzrest  17850  fclsfnflim  17980  flimfnfcls  17981  cnpfcf  17994  alexsubALTlem3  18001  alexsubALTlem4  18002  ptcmplem2  18005  ptcmplem5  18008  tsmsres  18094  restutop  18188  prdsxmetlem  18306  isxms2  18368  prdsbl  18411  met2ndci  18442  nmdvr  18577  nrginvrcnlem  18597  nrginvrcn  18598  tgqioo  18702  zdis  18718  reperflem  18720  reconnlem2  18729  reconn  18730  xrge0gsumle  18735  xrge0tsms  18736  xmetdcn  18740  metdcn  18742  metdscn2  18758  cncfmpt2ss  18816  icchmeo  18837  iccpnfcnv  18840  xrhmeo  18842  icccvx  18846  cnheibor  18851  bndth  18854  evth  18855  lebnum  18860  isphtpc  18890  reparphti  18893  pcoass  18920  nmoleub2lem  18993  nmoleub2lem3  18994  nmoleub2lem2  18995  nmoleub3  18998  nmhmcn  18999  cfili  19092  cfilfcls  19098  caussi  19121  equivcau  19124  minveclem4b  19199  minveclem4  19200  evthicc2  19224  ovolfcl  19230  ovolfioo  19231  ovolficc  19232  ovolficcss  19233  ovolfsval  19234  ovolmge0  19240  ovollb2lem  19251  ovolunlem1a  19259  ovoliunlem1  19265  ovolicc1  19279  ovolicc2lem4  19283  ovolicc2lem5  19284  ioombl1lem2  19320  ioombl1lem4  19322  ovolfs2  19330  ioorcl  19336  uniiccdif  19337  uniioovol  19338  uniiccvol  19339  uniioombllem2a  19341  uniioombllem2  19342  uniioombllem3a  19343  uniioombllem3  19344  uniioombllem4  19345  uniioombllem5  19346  uniioombllem6  19347  dyadmbl  19359  volsup2  19364  volivth  19366  vitalilem1  19367  vitalilem2  19368  vitalilem4  19370  mbfimaopnlem  19414  cncombf  19417  cnmbf  19418  mbflimsup  19425  mbfi1fseqlem3  19476  mbfi1fseqlem4  19477  mbfi1fseqlem5  19478  itg2const2  19500  itg2lea  19503  itg2eqa  19504  itg2split  19508  itg2i1fseq  19514  itg2gt0  19519  limcco  19647  dvcl  19653  perfdvf  19657  dvreslem  19663  dvres2lem  19664  dvidlem  19669  dvcnp2  19673  dvmulbr  19692  dvferm1lem  19735  dvferm2lem  19737  dvferm  19739  rolle  19741  dvlipcn  19745  dvlip2  19746  c1liplem1  19747  c1lip2  19749  dvgt0lem1  19753  dvivthlem1  19759  dvivth  19761  lhop1lem  19764  lhop1  19765  lhop2  19766  lhop  19767  dvfsumlem1  19777  dvfsumlem2  19778  dvfsumlem3  19779  dvfsumlem4  19780  dvfsumrlimge0  19781  dvfsumrlim  19782  dvfsumrlim2  19783  dvfsum2  19785  ftc1lem5  19791  ftc1lem6  19792  itgsubstlem  19799  itgsubst  19800  mdegleb  19854  mdegaddle  19864  mdegvsca  19866  mdegmullem  19868  ig1peu  19961  plybss  19980  plyaddcl  20006  plymulcl  20007  plysubcl  20008  coeidlem  20023  coesub  20042  dgrmulc  20056  dgrcolem1  20058  dgrcolem2  20059  dgrco  20060  quotlem  20084  quotcl2  20086  quotdgr  20087  plyrem  20089  facth  20090  quotcan  20093  vieta1lem1  20094  vieta1  20096  elqaalem3  20105  aalioulem2  20117  aalioulem3  20118  taylfvallem1  20140  tayl0  20145  dvntaylp  20154  taylthlem1  20156  taylthlem2  20157  radcnvlt1  20201  radcnvle  20203  pserulm  20205  psercnlem2  20207  psercnlem1  20208  psercn  20209  pserdvlem1  20210  pserdvlem2  20211  abelthlem3  20216  abelthlem5  20218  abelthlem6  20219  abelth  20224  efcvx  20232  tanord  20307  tanregt0  20308  efif1olem4  20314  logtayl  20418  logccv  20421  cxpcn3  20499  ssscongptld  20533  chordthmlem  20540  chordthmlem4  20543  chordthmlem5  20544  chordthm  20545  asinrecl  20609  atantan  20630  dvatan  20642  leibpi  20649  rlimcnp  20671  efrlim  20675  cvxcl  20690  scvxcvx  20691  jensenlem1  20692  jensenlem2  20693  jensen  20694  amgmlem  20695  harmonicbnd3  20713  wilthlem1  20718  ftalem3  20724  ftalem5  20726  ftalem7  20728  basellem3  20732  basellem4  20733  basellem5  20734  ppisval  20753  chtf  20758  efchtcl  20761  chtge0  20762  sgmval2  20793  ppinprm  20802  chtprm  20803  chtnprm  20804  chtwordi  20806  chtdif  20808  efchtdvds  20809  sqff1o  20832  fsumdvdsdiaglem  20835  fsumdvdsdiag  20836  fsumdvdscom  20837  musum  20843  muinv  20845  dvdsmulf1o  20846  sgmmul  20852  chtlepsi  20857  chtleppi  20861  pclogsum  20866  chpval2  20869  chpchtsum  20870  chpub  20871  perfectlem2  20881  dchrelbasd  20890  dchrrcl  20891  dchrzrh1  20895  dchrzrhmul  20897  dchrinvcl  20904  dchrfi  20906  dchrghm  20907  dchr1  20908  dchrabs  20911  dchrinv  20912  dchrptlem2  20916  dchrsum2  20919  sumdchr2  20921  sum2dchr  20925  lgscl  20961  lgsquadlem1  21005  lgsquadlem2  21006  2sqlem6  21020  2sqlem8  21023  2sqlem9  21024  chebbnd1lem1  21030  chtppilimlem1  21034  rplogsumlem2  21046  dchrisum0flblem1  21069  rpvmasum2  21073  dchrisum0re  21074  dchrisum0lema  21075  dchrisum0lem1b  21076  dchrisum0lem1  21077  dchrisum0lem2a  21078  dchrisum0lem2  21079  dchrisum0lem3  21080  dchrisum0  21081  rplogsum  21088  dirith2  21089  mudivsum  21091  mulogsum  21093  mulog2sumlem2  21096  vmalogdivsum2  21099  logsqvma  21103  logsqvma2  21104  selberglem3  21108  selberg  21109  chpdifbndlem1  21114  selberg34r  21132  pntsval2  21137  pntrlog2bndlem1  21138  pntpbnd1a  21146  pntpbnd1  21147  pntpbnd2  21148  pntibndlem2a  21151  pntibndlem2  21152  pntibndlem3  21153  pntlemd  21155  padicabv  21191  umgrass  21221  umgran0  21222  usgrass  21251  redwlk  21454  issubgo  21739  nvvop  21936  nmcnc  22040  ubthlem1  22220  minvecolem2  22225  minvecolem3  22226  minvecolem5  22231  minvecolem6  22232  minvecolem7  22233  hlimcaui  22587  pjocini  23048  eliccelico  23976  elicoelioo  23977  iundisjfi  23990  iundisj2fi  23991  divnumden2  23999  xrsmulgzz  24033  ressmulgnn  24034  ressmulgnn0  24035  xrge0addass  24040  xrge0addgt0  24043  xrge0adddir  24044  xrge0npcan  24045  fsumrp0cl  24046  xrge0tsmsd  24052  dvrdir  24055  rdivmuldivd  24056  dvrcan5  24058  elrhmunit  24074  rhmunitinv  24076  cnre2csqima  24113  tpr2rico  24114  cnvordtrestixx  24115  xrge0iifcnv  24123  xrge0iifhom  24127  xrge0mulc1cn  24131  rge0scvg  24139  lmxrge0  24141  qqhval2  24165  qqhvq  24170  qqhnm  24173  qqhcn  24174  qqhucn  24175  rrhre  24183  indsum  24216  indf1ofs  24219  esumel  24238  esumle  24245  esummono  24246  gsumesum  24247  esumlub  24248  esumlef  24250  esumcst  24251  esumfzf  24255  esumfsup  24256  esumfsupre  24257  esumpinfval  24259  esumpfinvallem  24260  esumpfinval  24261  esumpfinvalf  24262  esumpinfsum  24263  esumpcvgval  24264  esumpmono  24265  esummulc1  24267  esummulc2  24268  esumdivc  24269  hasheuni  24271  esumcvg  24272  sigainb  24315  measun  24359  measunl  24364  measiun  24366  meascnbl  24367  voliune  24379  volfiniune  24380  dya2icoseg2  24422  dya2iocnrect  24425  sxbrsigalem2  24430  probun  24456  probdif  24457  probvalrnd  24461  probmeasb  24467  cndprobin  24471  bayesth  24476  ballotlemsdom  24548  ballotlemrv2  24558  ballotlemfrci  24564  lgamgulmlem2  24593  lgamcvg2  24618  subfacp1lem5  24649  erdszelem4  24659  erdszelem6  24661  erdszelem7  24662  erdszelem8  24663  erdszelem9  24664  conpcon  24701  cvxscon  24709  rescon  24712  iccllyscon  24716  rellyscon  24717  cvmsrcl  24730  cvmliftmolem2  24748  cvmlift2lem12  24780  cvmlift3  24794  snmlval  24797  clim2prod  24995  ntrivcvg  25004  ntrivcvgfvn0  25006  ntrivcvgtail  25007  ntrivcvgmullem  25008  ntrivcvgmul  25009  prodrblem  25034  prodmolem2a  25039  axlowdimlem16  25610  axcontlem10  25626  itg2gt0cn  25960  ftc1cnnclem  25978  islocfin  26067  neibastop1  26079  fdc  26140  prdsbnd  26193  ismtyval  26200  heiborlem3  26213  heiborlem5  26215  heiborlem10  26220  rrnequiv  26235  eldiophb  26506  4rexfrabdioph  26549  6rexfrabdioph  26550  diophren  26565  rencldnfilem  26572  pellexlem3  26585  pellfundglb  26639  rmxypairf1o  26665  rmxycomplete  26671  rmxyneg  26674  rmxyadd  26675  rmxy1  26676  rmxy0  26677  monotuz  26695  jm2.22  26757  aomclem2  26821  isnumbasgrp  26941  dfacbasgrp  26942  hbtlem2  26997  hbt  27003  elmnc  27010  symggen  27080  symgtrinv  27082  psgnunilem5  27086  psgnunilem2  27087  psgnuni  27091  issdrg  27174  cntzsdrg  27179  mon1psubm  27194  stoweidlem26  27443  stoweidlem51  27468  suctrALT3  28377  chordthmALT  28387  bnj1213  28508  bnj1417  28748  osumcllem7N  30076  pexmidlem4N  30087
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
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 2374  df-cleq 2380  df-clel 2383  df-in 3270  df-ss 3277
  Copyright terms: Public domain W3C validator