Theorem sseldi 3487

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

Step	Hyp	Ref	Expression
1		sseldi.2	. 2 |- ( ph -> C e. A )
2		sseli.1	. . 3 |- A C_ B
3	2	sseli 3485	. 2 |- ( C e. A -> C e. B )
4	1, 3	syl 16	1 |- ( ph -> C e. B )

Syntax hints:   -> wi 4   e. wcel 1804   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475

This theorem is referenced by:  onfr  4907  sofld  5445  fvrn0  5878  riotacl  6257  riotasbc  6258  ovima0  6439  elmpt2cl  6502  ofrval  6535  opiota  6844  mpt2xopn0yelv  6943  mpt2xopxnop0  6945  tpostpos  6977  smores  7025  tz7.44-2  7075  omopthlem2  7307  f1opwfi  7826  supub  7921  suplub  7922  ordtypelem3  7948  ordtypelem4  7949  ordtypelem6  7951  ordtypelem7  7952  wemapsolem  7978  wemapso2OLD  7980  wemapso2lem  7981  unxpwdom2  8017  oemapvali  8106  wemapwe  8142  wemapweOLD  8143  oef1o  8144  oef1oOLD  8145  cnfcomlem  8146  cnfcomlemOLD  8154  r1pwss  8205  r1elwf  8217  rankr1ai  8219  r0weon  8393  infxpenlem  8394  acnlem  8432  acndom2  8438  infpwfien  8446  alephfp  8492  ackbij1b  8622  cflim2  8646  fin23lem26  8708  isf32lem5  8740  isf32lem7  8742  isf32lem8  8743  isf32lem9  8744  isfin1-3  8769  fin1a2lem9  8791  fin1a2lem11  8793  hsmexlem5  8813  zorn2lem3  8881  zorn2lem4  8882  zorn2lem5  8883  ttukeylem6  8897  ttukeylem7  8898  iundom2g  8918  fpwwe2lem12  9022  pwfseqlem3  9041  gch2  9056  wunom  9101  rexrd  9646  nnred  10558  nncnd  10559  un0addcl  10836  un0mulcl  10837  nnnn0d  10859  nn0red  10860  suprzcl  10949  nn0zd  10974  zred  10976  zsupss  11182  rpnnen1lem1  11219  rpnnen1lem2  11220  rpred  11267  supicclub2  11682  ige2m1fz  11779  zmodfzp1  12001  fzfi  12064  seqf1olem1  12128  expcl2lem  12160  m1expcl  12171  hashxrcl  12411  seqcoll2  12495  ccatrn  12588  swrdspsleq  12655  wrdeqcats1  12681  wrdind  12684  wrd2ind  12685  limsupgre  13286  rlimpm  13305  rlimclim  13351  isercolllem1  13469  isercolllem2  13470  isercoll  13472  iseraltlem2  13487  iseraltlem3  13488  zsum  13522  fsumcvg3  13533  ackbijnn  13622  clim2prod  13679  ntrivcvg  13688  ntrivcvgfvn0  13690  ntrivcvgtail  13691  ntrivcvgmullem  13692  ntrivcvgmul  13693  prodrblem  13718  prodmolem2a  13723  bitsval  14056  bitsfzolem  14066  bitsinv1  14074  smuval2  14114  gcdcllem3  14133  eulerthlem2  14294  prmdivdiv  14299  prmreclem1  14416  prmreclem2  14417  prmreclem3  14418  1arith  14427  4sqlem13  14457  4sqlem14  14458  4sqlem17  14461  vdwlem5  14485  vdwlem8  14488  vdwlem12  14492  vdwnnlem3  14497  ramtlecl  14500  ramcl2lem  14509  ramcl2  14516  ramxrcl  14517  submrc  15007  mreexexlem2d  15024  catlid  15062  catrid  15063  sscpwex  15166  subcrcl  15167  sscres  15174  wunfunc  15247  funcres2c  15249  cofull  15282  cofth  15283  coffth  15284  rescfth  15285  homarel  15342  arwrcl  15350  idaf  15369  homdmcoa  15373  coaval  15374  coapm  15377  catciso  15413  catcoppccl  15414  catcfuccl  15415  catcxpccl  15455  acsfiindd  15786  psssdm2  15824  gsumval2  15886  submrcl  15956  issubg  16180  isnsg  16209  nmzsubg  16221  conjnmz  16279  conjnmzb  16280  cntzsubm  16352  cntzsubg  16353  symggen  16474  symgtrinv  16476  psgnunilem5  16498  psgnunilem2  16499  psgnuni  16503  odlem2  16542  gexlem2  16581  sylow1lem2  16598  sylow1lem4  16600  sylow2a  16618  efglem  16713  efgtf  16719  efgtlen  16723  efgsres  16735  efgsfo  16736  efgredlemg  16739  efgredleme  16740  efgredlemd  16741  efgredlemc  16742  efgredlem  16744  efgred  16745  efgcpbllemb  16752  frgpuplem  16769  frgpnabllem2  16857  cyggex2  16878  dprdfsub  17040  dprdf11  17042  dprdfsubOLD  17047  dprdf11OLD  17049  dprd2da  17070  ablfac2  17119  issubrg  17408  cntzsubr  17440  abvrcl  17449  lbsextlem3  17785  sralmod  17812  rrgeq0  17917  psrbagconf1o  18005  psrass1lem  18008  psrdi  18040  psrdir  18041  psrass23l  18042  psrass23  18044  resspsrmul  18051  mplelf  18071  mplsubrglem  18079  mplsubrglemOLD  18080  mpladd  18083  mplmul  18084  mplvsca  18088  mplmonmul  18105  mplcoe5  18110  mplcoe2OLD  18112  mplind  18146  psropprmul  18258  ply1frcl  18334  rge0srg  18466  zringlpirlem2  18488  zringlpirlem3  18489  zlpirlem2  18493  zlpirlem3  18494  znf1o  18568  cygznlem2a  18584  psgninv  18596  ocvlss  18681  lsmcss  18701  isobs  18729  mdetralt  19088  neiptoptop  19610  restbas  19637  ordtbas2  19670  ordtopn1  19673  ordtopn2  19674  ordtrest  19681  iocpnfordt  19694  icomnfordt  19695  lmrcl  19710  subbascn  19733  lmss  19777  cnconn  19901  clscon  19909  concompclo  19914  subislly  19960  cldllycmp  19974  islocfin  19996  kgeni  20016  llycmpkgen2  20029  1stckgenlem  20032  ptbasfi  20060  xkoopn  20068  txcls  20083  dfac14lem  20096  txcnp  20099  ptcnplem  20100  upxp  20102  txtube  20119  txcmplem1  20120  txcmplem2  20121  txkgen  20131  xkopt  20134  xkococnlem  20138  txcon  20168  basqtop  20190  tgqtop  20191  kqnrmlem1  20222  kqnrmlem2  20223  nrmhmph  20273  ptcmpfi  20292  elmptrab  20306  uzrest  20376  fclsfnflim  20506  flimfnfcls  20507  cnpfcf  20520  alexsubALTlem3  20527  alexsubALTlem4  20528  ptcmplem2  20531  ptcmplem5  20534  tsmsresOLD  20623  tsmsres  20624  restutop  20718  prdsxmetlem  20849  isxms2  20929  prdsbl  20972  met2ndci  21003  nmdvr  21157  nrginvrcnlem  21177  nrginvrcn  21178  tgqioo  21283  zdis  21299  reperflem  21301  reconnlem2  21310  reconn  21311  xrge0gsumle  21316  xrge0tsms  21317  xmetdcn  21321  metdcn  21323  metdscn2  21339  cncfmpt2ss  21397  icchmeo  21419  iccpnfcnv  21422  xrhmeo  21424  icccvx  21428  cnheibor  21433  bndth  21436  evth  21437  lebnum  21442  isphtpc  21472  reparphti  21475  pcoass  21502  nmoleub2lem  21575  nmoleub2lem3  21576  nmoleub2lem2  21577  nmoleub3  21580  nmhmcn  21581  cfili  21685  cfilfcls  21691  caussi  21714  equivcau  21717  rrxf  21806  minveclem4b  21824  minveclem4  21825  evthicc2  21850  ovolfcl  21856  ovolfioo  21857  ovolficc  21858  ovolficcss  21859  ovolfsval  21860  ovolmge0  21866  ovollb2lem  21877  ovolunlem1a  21885  ovoliunlem1  21891  ovolicc1  21905  ovolicc2lem4  21909  ovolicc2lem5  21910  ioombl1lem2  21947  ioombl1lem4  21949  ovolfs2  21958  ioorcl  21964  uniiccdif  21965  uniioovol  21966  uniiccvol  21967  uniioombllem2a  21969  uniioombllem2  21970  uniioombllem3a  21971  uniioombllem3  21972  uniioombllem4  21973  uniioombllem5  21974  uniioombllem6  21975  dyadmbl  21987  volsup2  21992  volivth  21994  vitalilem1  21995  vitalilem2  21996  vitalilem4  21998  mbfimaopnlem  22040  cncombf  22043  cnmbf  22044  mbflimsup  22051  mbfi1fseqlem3  22102  mbfi1fseqlem4  22103  mbfi1fseqlem5  22104  itg2const2  22126  itg2lea  22129  itg2eqa  22130  itg2split  22134  itg2i1fseq  22140  itg2gt0  22145  limcco  22275  dvcl  22281  perfdvf  22285  dvreslem  22291  dvres2lem  22292  dvidlem  22297  dvcnp2  22301  dvmulbr  22320  dvferm1lem  22363  dvferm2lem  22365  dvferm  22367  rolle  22369  dvlipcn  22373  dvlip2  22374  c1liplem1  22375  c1lip2  22377  dvgt0lem1  22381  dvivthlem1  22387  dvivth  22389  lhop1lem  22392  lhop1  22393  lhop2  22394  lhop  22395  dvfsumlem1  22405  dvfsumlem2  22406  dvfsumlem3  22407  dvfsumlem4  22408  dvfsumrlimge0  22409  dvfsumrlim  22410  dvfsumrlim2  22411  dvfsum2  22413  ftc1lem5  22419  ftc1lem6  22420  itgsubstlem  22427  itgsubst  22428  mdegleb  22442  mdegaddle  22452  mdegvsca  22454  mdegmullem  22456  ig1peu  22550  plybss  22569  plyaddcl  22595  plymulcl  22596  plysubcl  22597  coeidlem  22612  coesub  22632  dgrmulc  22646  dgrcolem1  22648  dgrcolem2  22649  dgrco  22650  quotlem  22674  quotcl2  22676  quotdgr  22677  plyrem  22679  facth  22680  quotcan  22683  vieta1lem1  22684  vieta1  22686  elqaalem3  22695  aalioulem2  22707  aalioulem3  22708  taylfvallem1  22730  tayl0  22735  dvntaylp  22744  taylthlem1  22746  taylthlem2  22747  radcnvlt1  22791  radcnvle  22793  pserulm  22795  psercnlem2  22797  psercnlem1  22798  psercn  22799  pserdvlem1  22800  pserdvlem2  22801  abelthlem3  22806  abelthlem5  22808  abelthlem6  22809  abelth  22814  efcvx  22822  tanord  22903  tanregt0  22904  efif1olem4  22910  logtayl  23019  logccv  23022  cxpcn3  23100  ssscongptld  23134  chordthmlem  23141  chordthmlem4  23144  chordthmlem5  23145  chordthm  23146  heron  23147  asinrecl  23211  atantan  23232  dvatan  23244  leibpi  23251  rlimcnp  23273  efrlim  23277  cvxcl  23292  scvxcvx  23293  jensenlem1  23294  jensenlem2  23295  jensen  23296  amgmlem  23297  harmonicbnd3  23315  wilthlem1  23320  ftalem3  23326  ftalem5  23328  ftalem7  23330  basellem3  23334  basellem4  23335  basellem5  23336  ppisval  23355  chtf  23360  efchtcl  23363  chtge0  23364  sgmval2  23395  ppinprm  23404  chtprm  23405  chtnprm  23406  chtwordi  23408  chtdif  23410  efchtdvds  23411  sqff1o  23434  fsumdvdsdiaglem  23437  fsumdvdsdiag  23438  fsumdvdscom  23439  musum  23445  muinv  23447  dvdsmulf1o  23448  sgmmul  23454  chtlepsi  23459  chtleppi  23463  pclogsum  23468  chpval2  23471  chpchtsum  23472  chpub  23473  perfectlem2  23483  dchrelbasd  23492  dchrrcl  23493  dchrzrh1  23497  dchrzrhmul  23499  dchrinvcl  23506  dchrfi  23508  dchrghm  23509  dchr1  23510  dchrabs  23513  dchrinv  23514  dchrptlem2  23518  dchrsum2  23521  sumdchr2  23523  sum2dchr  23527  lgscl  23563  lgsquadlem1  23607  lgsquadlem2  23608  2sqlem6  23622  2sqlem8  23625  2sqlem9  23626  chebbnd1lem1  23632  chtppilimlem1  23636  rplogsumlem2  23648  dchrisum0flblem1  23671  rpvmasum2  23675  dchrisum0re  23676  dchrisum0lema  23677  dchrisum0lem1b  23678  dchrisum0lem1  23679  dchrisum0lem2a  23680  dchrisum0lem2  23681  dchrisum0lem3  23682  dchrisum0  23683  rplogsum  23690  dirith2  23691  mudivsum  23693  mulogsum  23695  mulog2sumlem2  23698  vmalogdivsum2  23701  logsqvma  23705  logsqvma2  23706  selberglem3  23710  selberg  23711  chpdifbndlem1  23716  selberg34r  23734  pntsval2  23739  pntrlog2bndlem1  23740  pntpbnd1a  23748  pntpbnd1  23749  pntpbnd2  23750  pntibndlem2a  23753  pntibndlem2  23754  pntibndlem3  23755  pntlemd  23757  padicabv  23793  axtgcgrrflx  23837  axtgcgrid  23838  axtgsegcon  23839  axtg5seg  23840  axtgbtwnid  23841  axtgpasch  23842  axtgcont1  23843  perpcom  24068  perpneq  24069  ragperp  24072  ttgcontlem1  24166  axlowdimlem16  24238  axcontlem10  24254  umgrass  24297  umgran0  24298  usgrass  24339  redwlk  24586  issubgo  25283  nvvop  25480  nmcnc  25584  ubthlem1  25764  minvecolem2  25769  minvecolem3  25770  minvecolem5  25775  minvecolem6  25776  minvecolem7  25777  hlimcaui  26132  pjocini  26594  fcnvgreu  27492  f1od2  27525  xrge0infss  27558  xrge0infssd  27559  eliccelico  27566  elicoelioo  27567  iundisjfi  27579  iundisj2fi  27580  divnumden2  27587  xrsmulgzz  27644  ressmulgnn  27649  ressmulgnn0  27650  xrge0addass  27656  xrge0addgt0  27659  xrge0adddir  27660  xrge0adddi  27661  xrge0npcan  27662  fsumrp0cl  27663  gsummpt2co  27749  xrge0tsmsd  27753  dvrdir  27758  rdivmuldivd  27759  dvrcan5  27761  elrhmunit  27788  rhmunitinv  27790  xrge0slmod  27812  cnre2csqima  27871  tpr2rico  27872  cnvordtrestixx  27873  ordtrestNEW  27881  xrge0iifcnv  27893  xrge0iifhom  27897  xrge0mulc1cn  27901  rge0scvg  27909  lmxrge0  27912  qqhval2  27941  qqhvq  27946  qqhnm  27949  qqhcn  27950  qqhucn  27951  indsum  28014  indf1ofs  28017  esumel  28036  esumle  28043  esummono  28044  gsumesum  28045  esumlub  28046  esumlef  28048  esumcst  28049  esumfzf  28053  esumfsup  28054  esumfsupre  28055  esumpinfval  28057  esumpfinvallem  28058  esumpfinval  28059  esumpfinvalf  28060  esumpinfsum  28061  esumpcvgval  28062  esumpmono  28063  esummulc1  28065  esummulc2  28066  esumdivc  28067  hasheuni  28069  esumcvg  28070  sigainb  28114  measun  28160  measunl  28165  measiun  28167  meascnbl  28168  voliune  28179  volfiniune  28180  ddemeas  28186  dya2icoseg2  28227  dya2iocnrect  28230  sxbrsigalem2  28235  oms0  28244  omsmon  28245  sibfof  28260  oddpwdc  28271  eulerpartlemgc  28279  eulerpartlemgvv  28293  eulerpartlemgf  28296  eulerpartlemgs2  28297  eulerpartlemn  28298  sseqf  28309  probun  28336  probdif  28337  probvalrnd  28341  probmeasb  28347  cndprobin  28351  bayesth  28356  ballotlemsdom  28428  ballotlemrv2  28438  ballotlemfrci  28444  sgnclre  28456  signswch  28496  signstf  28501  signsvtn0  28505  signsvfn  28517  signlem0  28522  lgamgulmlem2  28550  lgamcvg2  28575  subfacp1lem5  28606  erdszelem4  28616  erdszelem6  28618  erdszelem7  28619  erdszelem8  28620  erdszelem9  28621  conpcon  28658  cvxscon  28666  rescon  28669  iccllyscon  28673  rellyscon  28674  cvmsrcl  28687  cvmliftmolem2  28705  cvmlift2lem12  28737  cvmlift3  28751  snmlval  28754  mrsubvr  28849  msubff1  28894  mclsax  28907  mthmpps  28920  mclspps  28922  mblfinlem2  30028  itg2addnclem3  30044  itg2addnc  30045  itg2gt0cn  30046  ftc1cnnclem  30064  ftc1anclem6  30071  neibastop1  30153  fdc  30214  prdsbnd  30265  ismtyval  30272  heiborlem3  30285  heiborlem5  30287  heiborlem10  30292  rrnequiv  30307  eldiophb  30666  4rexfrabdioph  30707  6rexfrabdioph  30708  diophren  30723  rencldnfilem  30730  pellexlem3  30743  pellfundglb  30797  rmxypairf1o  30823  rmxycomplete  30829  rmxyneg  30832  rmxyadd  30833  rmxy1  30834  rmxy0  30835  monotuz  30853  jm2.22  30913  aomclem2  30977  isnumbasgrp  31032  dfacbasgrp  31033  hbtlem2  31049  hbt  31055  elmnc  31061  issdrg  31122  cntzsdrg  31127  mon1psubm  31142  lcmn0cl  31179  hashnzfz2  31202  evthiccabs  31483  mullimc  31576  limccog  31580  mullimcf  31583  limcperiod  31588  limcrecl  31589  sumnnodd  31590  ltmod  31598  limcresiooub  31602  limcresioolb  31603  limcleqr  31604  neglimc  31607  addlimc  31608  limclner  31611  sublimc  31612  reclimc  31613  limclr  31615  divlimc  31616  cncficcgt0  31645  cncfiooicclem1  31650  cncfiooicc  31651  cncfiooiccre  31652  cncfioobdlem  31653  cncfioobd  31654  fperdvper  31669  dvbdfbdioolem1  31679  ioodvbdlimc1lem1  31682  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvdmsscn  31687  dvnmptconst  31692  dvnxpaek  31693  dvnmul  31694  dvnprodlem3  31699  itgsincmulx  31727  itgioocnicc  31730  iblcncfioo  31731  stoweidlem26  31762  stoweidlem51  31787  dirkercncflem2  31840  fourierdlem1  31844  fourierdlem16  31859  fourierdlem18  31861  fourierdlem19  31862  fourierdlem20  31863  fourierdlem21  31864  fourierdlem22  31865  fourierdlem24  31867  fourierdlem25  31868  fourierdlem27  31870  fourierdlem31  31874  fourierdlem32  31875  fourierdlem33  31876  fourierdlem35  31878  fourierdlem37  31880  fourierdlem39  31882  fourierdlem41  31884  fourierdlem42  31885  fourierdlem46  31889  fourierdlem51  31894  fourierdlem60  31903  fourierdlem61  31904  fourierdlem62  31905  fourierdlem64  31907  fourierdlem65  31908  fourierdlem66  31909  fourierdlem68  31911  fourierdlem71  31914  fourierdlem73  31916  fourierdlem74  31917  fourierdlem75  31918  fourierdlem76  31919  fourierdlem78  31921  fourierdlem79  31922  fourierdlem81  31924  fourierdlem82  31925  fourierdlem83  31926  fourierdlem84  31927  fourierdlem85  31928  fourierdlem87  31930  fourierdlem88  31931  fourierdlem89  31932  fourierdlem91  31934  fourierdlem95  31938  fourierdlem101  31944  fourierdlem102  31945  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  fourierdlem112  31955  fourierdlem114  31957  fouriercnp  31963  fouriersw  31968  fouriercn  31969  elaa2lem  31970  elaa2  31971  etransclem23  31994  etransclem24  31995  etransclem25  31996  etransclem26  31997  etransclem28  31999  etransclem32  32003  etransclem34  32005  etransclem35  32006  etransclem37  32008  etransclem38  32009  etransclem44  32015  etransclem46  32017  etransclem48  32019  submgmrcl  32424  inclfusubc  32517  ply1ass23l  32852  suctrALT  33494  suctrALT3  33592  chordthmALT  33601  iunconlem2  33603  bnj1213  33725  bnj1417  33965  osumcllem7N  35561  pexmidlem4N  35572  cotr2g  37614  imo72b2  37797