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

Theorem sseldi 3179
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 3177 . 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 1685    C_ wss 3153
This theorem is referenced by:  onfr  4430  sofld  5120  fvrn0  5512  elmpt2cl  6023  ofrval  6050  tpostpos  6216  opiota  6284  riotacl  6315  riotasbc  6316  smores  6365  tz7.44-2  6416  omopthlem2  6650  f1opwfi  7155  supub  7206  suplub  7207  ordtypelem3  7231  ordtypelem4  7232  ordtypelem6  7234  ordtypelem7  7235  wemapso2lem  7261  wemapso2  7263  unxpwdom2  7298  cantnfres  7375  wemapwe  7396  oef1o  7397  cnfcomlem  7398  r1pwss  7452  r1elwf  7464  rankr1ai  7466  r0weon  7636  infxpenlem  7637  acnlem  7671  acndom2  7677  infpwfien  7685  alephfp  7731  ackbij1lem18  7859  ackbij1b  7861  cflim2  7885  fin23lem26  7947  fin23lem30  7964  isf32lem5  7979  isf32lem7  7981  isf32lem8  7982  isf32lem9  7983  isfin1-3  8008  fin1a2lem9  8030  fin1a2lem11  8032  hsmexlem5  8052  zorn2lem3  8121  zorn2lem4  8122  zorn2lem5  8123  ttukeylem6  8137  ttukeylem7  8138  iundom2g  8158  fpwwe2lem12  8259  pwfseqlem3  8278  gch2  8297  wunom  8338  rexrd  8877  nnred  9757  nncnd  9758  un0addcl  9993  un0mulcl  9994  nnnn0d  10014  nn0red  10015  suprzcl  10087  nn0zd  10111  zred  10113  zsupss  10303  rpnnen1lem1  10338  rpnnen1lem2  10339  rpred  10386  fzfi  11030  seqf1olem1  11081  expcl2lem  11111  m1expcl  11122  hashxrcl  11347  seqcoll2  11398  wrdeqcats1  11470  wrdind  11473  limsupgre  11951  rlimpm  11970  rlimclim  12016  isercolllem1  12134  isercolllem2  12135  isercoll  12137  iseraltlem2  12151  iseraltlem3  12152  fsumcvg3  12198  ackbijnn  12282  bitsval  12611  bitsfzolem  12621  bitsinv1  12629  smuval2  12669  gcdcllem3  12688  eulerthlem2  12846  prmdivdiv  12851  prmreclem1  12959  prmreclem2  12960  prmreclem3  12961  1arith  12970  4sqlem13  13000  4sqlem14  13001  4sqlem17  13004  vdwlem5  13028  vdwlem8  13031  vdwlem12  13035  vdwnnlem3  13040  ramtlecl  13043  ramcl2lem  13052  ramcl2  13059  ramxrcl  13060  submrc  13526  mreexexlem2d  13543  catlid  13581  catrid  13582  sscpwex  13688  subcrcl  13689  sscres  13696  wunfunc  13769  funcres2c  13771  cofull  13804  cofth  13805  coffth  13806  rescfth  13807  homarel  13864  arwrcl  13872  idaf  13891  homdmcoa  13895  coaval  13896  coapm  13899  catciso  13935  catcoppccl  13936  catcfuccl  13937  catcxpccl  13977  acsfiindd  14276  psssdm2  14320  submrcl  14420  gsumval2  14456  issubg  14617  isnsg  14642  nmzsubg  14654  conjnmz  14712  conjnmzb  14713  cntzsubm  14807  cntzsubg  14808  odlem2  14850  gexlem2  14889  sylow1lem2  14906  sylow1lem4  14908  sylow2a  14926  efglem  15021  efgtf  15027  efgtlen  15031  efgsres  15043  efgsfo  15044  efgredlemg  15047  efgredleme  15048  efgredlemd  15049  efgredlemc  15050  efgredlem  15052  efgred  15053  efgcpbllemb  15060  frgpuplem  15077  frgpnabllem2  15158  cyggex2  15179  dprdfsub  15252  dprdf11  15254  dprd2da  15273  ablfac2  15320  isdrng2  15518  issubrg  15541  cntzsubr  15573  abvrcl  15582  lsppratlem1  15896  lsppratlem2  15897  lbsextlem3  15909  sralmod  15935  rrgeq0  16027  psrbagconf1o  16116  psrass1lem  16119  psrdi  16147  psrdir  16148  psrass23  16150  resspsrmul  16157  mplelf  16174  mplsubrglem  16179  mpladd  16182  mplmul  16183  mplvsca  16187  mplmonmul  16204  mplcoe2  16207  mplind  16239  psropprmul  16312  zlpirlem2  16438  zlpirlem3  16439  znf1o  16501  cygznlem2a  16517  ocvlss  16568  lsmcss  16588  isobs  16616  restbas  16885  ordtbas2  16917  ordtopn1  16920  ordtopn2  16921  ordtrest  16928  iocpnfordt  16941  icomnfordt  16942  lmrcl  16957  subbascn  16980  lmss  17022  hauscmplem  17129  cnconn  17144  clscon  17152  concompclo  17157  subislly  17203  cldllycmp  17217  kgeni  17228  llycmpkgen2  17241  1stckgenlem  17244  ptbasfi  17272  xkoopn  17280  txcls  17295  dfac14lem  17307  txcnp  17310  ptcnplem  17311  upxp  17313  txtube  17330  txcmplem1  17331  txcmplem2  17332  txkgen  17342  xkopt  17345  xkococnlem  17349  txcon  17379  basqtop  17398  tgqtop  17399  kqnrmlem1  17430  kqnrmlem2  17431  nrmhmph  17481  ptcmpfi  17500  elmptrab  17518  uzrest  17588  fclsfnflim  17718  flimfnfcls  17719  cnpfcf  17732  alexsubALTlem3  17739  alexsubALTlem4  17740  ptcmplem2  17743  ptcmplem5  17746  tsmsres  17822  prdsxmetlem  17928  imasdsf1olem  17933  isxms2  17990  prdsbl  18033  met2ndci  18064  nmdvr  18177  nrginvrcnlem  18197  nrginvrcn  18198  tgqioo  18302  zdis  18318  reperflem  18319  reconnlem2  18328  reconn  18329  xrge0gsumle  18334  xrge0tsms  18335  xmetdcn  18339  metdcn  18341  metdscn2  18357  cncfmpt2ss  18415  icchmeo  18435  iccpnfcnv  18438  xrhmeo  18440  icccvx  18444  cnheibor  18449  bndth  18452  evth  18453  lebnum  18458  isphtpc  18488  reparphti  18491  pcoass  18518  nmoleub2lem  18591  nmoleub2lem3  18592  nmoleub2lem2  18593  nmoleub3  18596  nmhmcn  18597  cfili  18690  cfilfcls  18696  caussi  18719  equivcau  18722  minveclem4b  18791  minveclem4  18792  evthicc2  18816  ovolfcl  18822  ovolfioo  18823  ovolficc  18824  ovolficcss  18825  ovolfsval  18826  ovolmge0  18832  ovollb2lem  18843  ovolunlem1a  18851  ovoliunlem1  18857  ovolicc1  18871  ovolicc2lem4  18875  ovolicc2lem5  18876  ioombl1lem2  18912  ioombl1lem4  18914  ovolfs2  18922  ioorcl  18928  uniiccdif  18929  uniioovol  18930  uniiccvol  18931  uniioombllem2a  18933  uniioombllem2  18934  uniioombllem3a  18935  uniioombllem3  18936  uniioombllem4  18937  uniioombllem5  18938  uniioombllem6  18939  dyadmbl  18951  volsup2  18956  volivth  18958  vitalilem1  18959  vitalilem2  18960  vitalilem4  18962  mbfimaopnlem  19006  cncombf  19009  cnmbf  19010  mbflimsup  19017  mbfi1fseqlem3  19068  mbfi1fseqlem4  19069  mbfi1fseqlem5  19070  itg2const2  19092  itg2lea  19095  itg2eqa  19096  itg2split  19100  itg2i1fseq  19106  itg2gt0  19111  limcco  19239  dvcl  19245  perfdvf  19249  dvreslem  19255  dvres2lem  19256  dvidlem  19261  dvcnp2  19265  dvmulbr  19284  dvrec  19300  dvferm1lem  19327  dvferm2lem  19329  dvferm  19331  rolle  19333  dvlipcn  19337  dvlip2  19338  c1liplem1  19339  c1lip2  19341  dvgt0lem1  19345  dvivthlem1  19351  dvivth  19353  lhop1lem  19356  lhop1  19357  lhop2  19358  lhop  19359  dvfsumlem1  19369  dvfsumlem2  19370  dvfsumlem3  19371  dvfsumlem4  19372  dvfsumrlimge0  19373  dvfsumrlim  19374  dvfsumrlim2  19375  dvfsum2  19377  ftc1lem5  19383  ftc1lem6  19384  itgsubstlem  19391  itgsubst  19392  mdegleb  19446  mdegaddle  19456  mdegvsca  19458  mdegmullem  19460  ig1peu  19553  plybss  19572  plyaddcl  19598  plymulcl  19599  plysubcl  19600  coeidlem  19615  coesub  19634  dgrmulc  19648  dgrcolem1  19650  dgrcolem2  19651  dgrco  19652  quotlem  19676  quotcl2  19678  quotdgr  19679  plyrem  19681  facth  19682  quotcan  19685  vieta1lem1  19686  vieta1  19688  elqaalem3  19697  aalioulem2  19709  aalioulem3  19710  taylfvallem1  19732  tayl0  19737  dvntaylp  19746  taylthlem1  19748  taylthlem2  19749  radcnvlt1  19790  radcnvle  19792  pserulm  19794  psercnlem2  19796  psercnlem1  19797  psercn  19798  pserdvlem1  19799  pserdvlem2  19800  abelthlem3  19805  abelthlem5  19807  abelthlem6  19808  abelth  19813  efcvx  19821  tanord  19896  tanregt0  19897  efif1olem4  19903  logtayl  20003  logccv  20006  cxpcn3  20084  ssscongptld  20118  chordthmlem  20125  chordthmlem4  20128  chordthmlem5  20129  chordthm  20130  asinrecl  20194  atantan  20215  dvatan  20227  leibpi  20234  rlimcnp  20256  efrlim  20260  cvxcl  20275  scvxcvx  20276  jensenlem1  20277  jensenlem2  20278  jensen  20279  amgmlem  20280  harmonicbnd3  20297  wilthlem1  20302  ftalem3  20308  ftalem5  20310  ftalem7  20312  basellem3  20316  basellem4  20317  basellem5  20318  ppisval  20337  chtf  20342  efchtcl  20345  chtge0  20346  sgmval2  20377  ppinprm  20386  chtprm  20387  chtnprm  20388  chtwordi  20390  chtdif  20392  efchtdvds  20393  sqff1o  20416  fsumdvdsdiaglem  20419  fsumdvdsdiag  20420  fsumdvdscom  20421  musum  20427  muinv  20429  dvdsmulf1o  20430  sgmmul  20436  chtlepsi  20441  chtleppi  20445  pclogsum  20450  chpval2  20453  chpchtsum  20454  chpub  20455  perfectlem2  20465  dchrelbasd  20474  dchrrcl  20475  dchrzrh1  20479  dchrzrhmul  20481  dchrinvcl  20488  dchrfi  20490  dchrghm  20491  dchr1  20492  dchrabs  20495  dchrinv  20496  dchrptlem2  20500  dchrsum2  20503  sumdchr2  20505  sum2dchr  20509  lgscl  20545  lgsquadlem1  20589  lgsquadlem2  20590  2sqlem6  20604  2sqlem8  20607  2sqlem9  20608  chebbnd1lem1  20614  chtppilimlem1  20618  rplogsumlem2  20630  dchrisum0flblem1  20653  rpvmasum2  20657  dchrisum0re  20658  dchrisum0lema  20659  dchrisum0lem1b  20660  dchrisum0lem1  20661  dchrisum0lem2a  20662  dchrisum0lem2  20663  dchrisum0lem3  20664  dchrisum0  20665  rplogsum  20672  dirith2  20673  mudivsum  20675  mulogsum  20677  mulog2sumlem2  20680  vmalogdivsum2  20683  logsqvma  20687  logsqvma2  20688  selberglem3  20692  selberg  20693  chpdifbndlem1  20698  selberg34r  20716  pntsval2  20721  pntrlog2bndlem1  20722  pntpbnd1a  20730  pntpbnd1  20731  pntpbnd2  20732  pntibndlem2a  20735  pntibndlem2  20736  pntibndlem3  20737  pntlemd  20739  padicabv  20775  issubgo  20964  nvvop  21159  nmcnc  21263  ubthlem1  21443  minvecolem2  21448  minvecolem3  21449  minvecolem5  21454  minvecolem6  21455  minvecolem7  21456  hlimcaui  21812  pjocini  22273  ballotlemfc0  23047  ballotlemfcc  23048  ballotlemimin  23060  ballotlemsdom  23066  ballotlemrv2  23076  ballotlemfrci  23082  subfacp1lem5  23122  erdszelem4  23132  erdszelem6  23134  erdszelem7  23135  erdszelem8  23136  erdszelem9  23137  conpcon  23173  cvxscon  23181  rescon  23184  iccllyscon  23188  rellyscon  23189  cvmsrcl  23202  cvmliftmolem2  23220  cvmlift2lem12  23252  cvmlift3  23266  umgrass  23278  umgran0  23279  umgraex  23282  snmlval  23321  axfelem13  23762  axlowdimlem16  23995  axcontlem10  24011  inposet  24689  besubbeca  25259  pfsubkl  25458  islocfin  25707  neibastop1  25719  fdc  25866  prdsbnd  25928  ismtyval  25935  heiborlem3  25948  heiborlem5  25950  heiborlem10  25955  rrnequiv  25970  eldiophb  26247  4rexfrabdioph  26290  6rexfrabdioph  26291  diophren  26307  rencldnfilem  26314  pellexlem3  26327  pellfundglb  26381  rmxypairf1o  26407  rmxycomplete  26413  rmxyneg  26416  rmxyadd  26417  rmxy1  26418  rmxy0  26419  monotuz  26437  jm2.22  26499  aomclem2  26563  isnumbasgrp  26683  dfacbasgrp  26684  hbtlem2  26739  hbt  26745  elmnc  26752  pmtrfinv  26813  symggen  26822  symgtrinv  26824  psgnunilem5  26828  psgnunilem2  26829  psgnuni  26833  issdrg  26916  cntzsdrg  26921  mon1psubm  26936  wallispilem4  27228  suctrALT3  27980  bnj1213  28110  bnj1417  28350  osumcllem7N  29430  pexmidlem4N  29441
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator