Theorem sseldi 3349

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 3347	. 2 |- ( C e. A -> C e. B )
4	1, 3	syl 16	1 |- ( ph -> C e. B )

Syntax hints:   -> wi 4   e. wcel 1756   C_ wss 3323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337

This theorem is referenced by:  onfr  4753  sofld  5281  fvrn0  5707  riotacl  6062  riotasbc  6063  elmpt2cl  6299  ofrval  6325  opiota  6628  mpt2xopn0yelv  6725  mpt2xopxnop0  6727  tpostpos  6760  smores  6805  tz7.44-2  6855  omopthlem2  7087  f1opwfi  7607  supub  7701  suplub  7702  ordtypelem3  7726  ordtypelem4  7727  ordtypelem6  7729  ordtypelem7  7730  wemapsolem  7756  wemapso2OLD  7758  wemapso2lem  7759  unxpwdom2  7795  oemapvali  7884  wemapwe  7920  wemapweOLD  7921  oef1o  7922  oef1oOLD  7923  cnfcomlem  7924  cnfcomlemOLD  7932  r1pwss  7983  r1elwf  7995  rankr1ai  7997  r0weon  8171  infxpenlem  8172  acnlem  8210  acndom2  8216  infpwfien  8224  alephfp  8270  ackbij1b  8400  cflim2  8424  fin23lem26  8486  isf32lem5  8518  isf32lem7  8520  isf32lem8  8521  isf32lem9  8522  isfin1-3  8547  fin1a2lem9  8569  fin1a2lem11  8571  hsmexlem5  8591  zorn2lem3  8659  zorn2lem4  8660  zorn2lem5  8661  ttukeylem6  8675  ttukeylem7  8676  iundom2g  8696  fpwwe2lem12  8800  pwfseqlem3  8819  gch2  8834  wunom  8879  rexrd  9425  nnred  10329  nncnd  10330  un0addcl  10605  un0mulcl  10606  nnnn0d  10628  nn0red  10629  suprzcl  10713  nn0zd  10737  zred  10739  zsupss  10936  rpnnen1lem1  10971  rpnnen1lem2  10972  rpred  11019  supicclub2  11428  zmodfzp1  11723  fzfi  11786  seqf1olem1  11837  expcl2lem  11869  m1expcl  11880  hashxrcl  12119  seqcoll2  12209  swrdspsleq  12334  wrdeqcats1  12360  wrdind  12363  wrd2ind  12364  limsupgre  12951  rlimpm  12970  rlimclim  13016  isercolllem1  13134  isercolllem2  13135  isercoll  13137  iseraltlem2  13152  iseraltlem3  13153  zsum  13187  fsumcvg3  13198  ackbijnn  13283  bitsval  13612  bitsfzolem  13622  bitsinv1  13630  smuval2  13670  gcdcllem3  13689  eulerthlem2  13849  prmdivdiv  13854  prmreclem1  13969  prmreclem2  13970  prmreclem3  13971  1arith  13980  4sqlem13  14010  4sqlem14  14011  4sqlem17  14014  vdwlem5  14038  vdwlem8  14041  vdwlem12  14045  vdwnnlem3  14050  ramtlecl  14053  ramcl2lem  14062  ramcl2  14069  ramxrcl  14070  submrc  14558  mreexexlem2d  14575  catlid  14613  catrid  14614  sscpwex  14720  subcrcl  14721  sscres  14728  wunfunc  14801  funcres2c  14803  cofull  14836  cofth  14837  coffth  14838  rescfth  14839  homarel  14896  arwrcl  14904  idaf  14923  homdmcoa  14927  coaval  14928  coapm  14931  catciso  14967  catcoppccl  14968  catcfuccl  14969  catcxpccl  15009  acsfiindd  15339  psssdm2  15377  submrcl  15465  gsumval2  15504  issubg  15672  isnsg  15701  nmzsubg  15713  conjnmz  15771  conjnmzb  15772  cntzsubm  15844  cntzsubg  15845  symggen  15967  symgtrinv  15969  psgnunilem5  15991  psgnunilem2  15992  psgnuni  15996  odlem2  16033  gexlem2  16072  sylow1lem2  16089  sylow1lem4  16091  sylow2a  16109  efglem  16204  efgtf  16210  efgtlen  16214  efgsres  16226  efgsfo  16227  efgredlemg  16230  efgredleme  16231  efgredlemd  16232  efgredlemc  16233  efgredlem  16235  efgred  16236  efgcpbllemb  16243  frgpuplem  16260  frgpnabllem2  16343  cyggex2  16364  dprdfsub  16499  dprdf11  16501  dprdfsubOLD  16506  dprdf11OLD  16508  dprd2da  16529  ablfac2  16578  issubrg  16843  cntzsubr  16875  abvrcl  16884  lbsextlem3  17218  sralmod  17245  rrgeq0  17338  psrbagconf1o  17421  psrass1lem  17424  psrdi  17456  psrdir  17457  psrass23  17459  resspsrmul  17466  mplelf  17486  mplsubrglem  17494  mplsubrglemOLD  17495  mpladd  17498  mplmul  17499  mplvsca  17503  mplmonmul  17520  mplcoe2  17524  mplcoe2OLD  17525  mplind  17559  psropprmul  17668  ply1frcl  17728  nn0srg  17856  rge0srg  17857  zringlpirlem2  17879  zringlpirlem3  17880  zlpirlem2  17884  zlpirlem3  17885  znf1o  17959  cygznlem2a  17975  psgninv  17987  ocvlss  18072  lsmcss  18092  isobs  18120  mdetralt  18389  neiptoptop  18710  restbas  18737  ordtbas2  18770  ordtopn1  18773  ordtopn2  18774  ordtrest  18781  iocpnfordt  18794  icomnfordt  18795  lmrcl  18810  subbascn  18833  lmss  18877  cnconn  19001  clscon  19009  concompclo  19014  subislly  19060  cldllycmp  19074  kgeni  19085  llycmpkgen2  19098  1stckgenlem  19101  ptbasfi  19129  xkoopn  19137  txcls  19152  dfac14lem  19165  txcnp  19168  ptcnplem  19169  upxp  19171  txtube  19188  txcmplem1  19189  txcmplem2  19190  txkgen  19200  xkopt  19203  xkococnlem  19207  txcon  19237  basqtop  19259  tgqtop  19260  kqnrmlem1  19291  kqnrmlem2  19292  nrmhmph  19342  ptcmpfi  19361  elmptrab  19375  uzrest  19445  fclsfnflim  19575  flimfnfcls  19576  cnpfcf  19589  alexsubALTlem3  19596  alexsubALTlem4  19597  ptcmplem2  19600  ptcmplem5  19603  tsmsresOLD  19692  tsmsres  19693  restutop  19787  prdsxmetlem  19918  isxms2  19998  prdsbl  20041  met2ndci  20072  nmdvr  20226  nrginvrcnlem  20246  nrginvrcn  20247  tgqioo  20352  zdis  20368  reperflem  20370  reconnlem2  20379  reconn  20380  xrge0gsumle  20385  xrge0tsms  20386  xmetdcn  20390  metdcn  20392  metdscn2  20408  cncfmpt2ss  20466  icchmeo  20488  iccpnfcnv  20491  xrhmeo  20493  icccvx  20497  cnheibor  20502  bndth  20505  evth  20506  lebnum  20511  isphtpc  20541  reparphti  20544  pcoass  20571  nmoleub2lem  20644  nmoleub2lem3  20645  nmoleub2lem2  20646  nmoleub3  20649  nmhmcn  20650  cfili  20754  cfilfcls  20760  caussi  20783  equivcau  20786  rrxf  20875  minveclem4b  20893  minveclem4  20894  evthicc2  20919  ovolfcl  20925  ovolfioo  20926  ovolficc  20927  ovolficcss  20928  ovolfsval  20929  ovolmge0  20935  ovollb2lem  20946  ovolunlem1a  20954  ovoliunlem1  20960  ovolicc1  20974  ovolicc2lem4  20978  ovolicc2lem5  20979  ioombl1lem2  21015  ioombl1lem4  21017  ovolfs2  21026  ioorcl  21032  uniiccdif  21033  uniioovol  21034  uniiccvol  21035  uniioombllem2a  21037  uniioombllem2  21038  uniioombllem3a  21039  uniioombllem3  21040  uniioombllem4  21041  uniioombllem5  21042  uniioombllem6  21043  dyadmbl  21055  volsup2  21060  volivth  21062  vitalilem1  21063  vitalilem2  21064  vitalilem4  21066  mbfimaopnlem  21108  cncombf  21111  cnmbf  21112  mbflimsup  21119  mbfi1fseqlem3  21170  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  itg2const2  21194  itg2lea  21197  itg2eqa  21198  itg2split  21202  itg2i1fseq  21208  itg2gt0  21213  limcco  21343  dvcl  21349  perfdvf  21353  dvreslem  21359  dvres2lem  21360  dvidlem  21365  dvcnp2  21369  dvmulbr  21388  dvferm1lem  21431  dvferm2lem  21433  dvferm  21435  rolle  21437  dvlipcn  21441  dvlip2  21442  c1liplem1  21443  c1lip2  21445  dvgt0lem1  21449  dvivthlem1  21455  dvivth  21457  lhop1lem  21460  lhop1  21461  lhop2  21462  lhop  21463  dvfsumlem1  21473  dvfsumlem2  21474  dvfsumlem3  21475  dvfsumlem4  21476  dvfsumrlimge0  21477  dvfsumrlim  21478  dvfsumrlim2  21479  dvfsum2  21481  ftc1lem5  21487  ftc1lem6  21488  itgsubstlem  21495  itgsubst  21496  mdegleb  21510  mdegaddle  21520  mdegvsca  21522  mdegmullem  21524  ig1peu  21618  plybss  21637  plyaddcl  21663  plymulcl  21664  plysubcl  21665  coeidlem  21680  coesub  21699  dgrmulc  21713  dgrcolem1  21715  dgrcolem2  21716  dgrco  21717  quotlem  21741  quotcl2  21743  quotdgr  21744  plyrem  21746  facth  21747  quotcan  21750  vieta1lem1  21751  vieta1  21753  elqaalem3  21762  aalioulem2  21774  aalioulem3  21775  taylfvallem1  21797  tayl0  21802  dvntaylp  21811  taylthlem1  21813  taylthlem2  21814  radcnvlt1  21858  radcnvle  21860  pserulm  21862  psercnlem2  21864  psercnlem1  21865  psercn  21866  pserdvlem1  21867  pserdvlem2  21868  abelthlem3  21873  abelthlem5  21875  abelthlem6  21876  abelth  21881  efcvx  21889  tanord  21969  tanregt0  21970  efif1olem4  21976  logtayl  22080  logccv  22083  cxpcn3  22161  ssscongptld  22195  chordthmlem  22202  chordthmlem4  22205  chordthmlem5  22206  chordthm  22207  heron  22208  asinrecl  22272  atantan  22293  dvatan  22305  leibpi  22312  rlimcnp  22334  efrlim  22338  cvxcl  22353  scvxcvx  22354  jensenlem1  22355  jensenlem2  22356  jensen  22357  amgmlem  22358  harmonicbnd3  22376  wilthlem1  22381  ftalem3  22387  ftalem5  22389  ftalem7  22391  basellem3  22395  basellem4  22396  basellem5  22397  ppisval  22416  chtf  22421  efchtcl  22424  chtge0  22425  sgmval2  22456  ppinprm  22465  chtprm  22466  chtnprm  22467  chtwordi  22469  chtdif  22471  efchtdvds  22472  sqff1o  22495  fsumdvdsdiaglem  22498  fsumdvdsdiag  22499  fsumdvdscom  22500  musum  22506  muinv  22508  dvdsmulf1o  22509  sgmmul  22515  chtlepsi  22520  chtleppi  22524  pclogsum  22529  chpval2  22532  chpchtsum  22533  chpub  22534  perfectlem2  22544  dchrelbasd  22553  dchrrcl  22554  dchrzrh1  22558  dchrzrhmul  22560  dchrinvcl  22567  dchrfi  22569  dchrghm  22570  dchr1  22571  dchrabs  22574  dchrinv  22575  dchrptlem2  22579  dchrsum2  22582  sumdchr2  22584  sum2dchr  22588  lgscl  22624  lgsquadlem1  22668  lgsquadlem2  22669  2sqlem6  22683  2sqlem8  22686  2sqlem9  22687  chebbnd1lem1  22693  chtppilimlem1  22697  rplogsumlem2  22709  dchrisum0flblem1  22732  rpvmasum2  22736  dchrisum0re  22737  dchrisum0lema  22738  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2a  22741  dchrisum0lem2  22742  dchrisum0lem3  22743  dchrisum0  22744  rplogsum  22751  dirith2  22752  mudivsum  22754  mulogsum  22756  mulog2sumlem2  22759  vmalogdivsum2  22762  logsqvma  22766  logsqvma2  22767  selberglem3  22771  selberg  22772  chpdifbndlem1  22777  selberg34r  22795  pntsval2  22800  pntrlog2bndlem1  22801  pntpbnd1a  22809  pntpbnd1  22810  pntpbnd2  22811  pntibndlem2a  22814  pntibndlem2  22815  pntibndlem3  22816  pntlemd  22818  padicabv  22854  axtgcgrrflx  22898  axtgcgrid  22899  axtgsegcon  22900  axtg5seg  22901  axtgbtwnid  22902  axtgpasch  22903  axtgcont1  22904  ttgcontlem1  23082  axlowdimlem16  23154  axcontlem10  23170  umgrass  23204  umgran0  23205  usgrass  23234  redwlk  23456  issubgo  23741  nvvop  23938  nmcnc  24042  ubthlem1  24222  minvecolem2  24227  minvecolem3  24228  minvecolem5  24233  minvecolem6  24234  minvecolem7  24235  hlimcaui  24590  pjocini  25052  fcnvgreu  25942  f1od2  25975  xrge0infss  26004  xrge0infssd  26005  eliccelico  26018  elicoelioo  26019  iundisjfi  26031  iundisj2fi  26032  divnumden2  26038  xrsmulgzz  26090  ressmulgnn  26095  ressmulgnn0  26096  xrge0addass  26102  xrge0addgt0  26105  xrge0adddir  26106  xrge0adddi  26107  xrge0npcan  26108  fsumrp0cl  26109  archirngz  26157  archiabllem1b  26160  gsummpt2co  26200  regsumfsum  26201  xrge0tsmsd  26204  dvrdir  26209  rdivmuldivd  26210  dvrcan5  26212  elrhmunit  26239  rhmunitinv  26241  xrge0slmod  26264  cnre2csqima  26293  tpr2rico  26294  cnvordtrestixx  26295  ordtrestNEW  26303  xrge0iifcnv  26315  xrge0iifhom  26319  xrge0mulc1cn  26323  rge0scvg  26331  lmxrge0  26334  cnzh  26351  rezh  26352  qqhval2  26363  qqhvq  26368  qqhnm  26371  qqhcn  26372  qqhucn  26373  indsum  26431  indf1ofs  26434  esumel  26453  esumle  26460  esummono  26461  gsumesum  26462  esumlub  26463  esumlef  26465  esumcst  26466  esumfzf  26470  esumfsup  26471  esumfsupre  26472  esumpinfval  26474  esumpfinvallem  26475  esumpfinval  26476  esumpfinvalf  26477  esumpinfsum  26478  esumpcvgval  26479  esumpmono  26480  esummulc1  26482  esummulc2  26483  esumdivc  26484  hasheuni  26486  esumcvg  26487  sigainb  26531  measun  26577  measunl  26582  measiun  26584  meascnbl  26585  voliune  26597  volfiniune  26598  ddemeas  26604  dya2icoseg2  26645  dya2iocnrect  26648  sxbrsigalem2  26653  oms0  26662  omsmon  26663  sibfof  26678  oddpwdc  26689  eulerpartlemgc  26697  eulerpartlemgvv  26711  eulerpartlemgf  26714  eulerpartlemgs2  26715  eulerpartlemn  26716  sseqf  26727  probun  26754  probdif  26755  probvalrnd  26759  probmeasb  26765  cndprobin  26769  bayesth  26774  ballotlemsdom  26846  ballotlemrv2  26856  ballotlemfrci  26862  sgnclre  26874  plymulx0  26900  signsply0  26904  signswch  26914  signstf  26919  signsvtn0  26923  signsvfn  26935  signlem0  26940  lgamgulmlem2  26968  lgamcvg2  26993  subfacp1lem5  27024  erdszelem4  27034  erdszelem6  27036  erdszelem7  27037  erdszelem8  27038  erdszelem9  27039  conpcon  27076  cvxscon  27084  rescon  27087  iccllyscon  27091  rellyscon  27092  cvmsrcl  27105  cvmliftmolem2  27123  cvmlift2lem12  27155  cvmlift3  27169  snmlval  27172  clim2prod  27354  ntrivcvg  27363  ntrivcvgfvn0  27365  ntrivcvgtail  27366  ntrivcvgmullem  27367  ntrivcvgmul  27368  prodrblem  27393  prodmolem2a  27398  mblfinlem2  28382  itg2addnclem3  28398  itg2addnc  28399  itg2gt0cn  28400  ftc1cnnclem  28418  ftc1anclem6  28425  islocfin  28521  neibastop1  28533  fdc  28594  prdsbnd  28645  ismtyval  28652  heiborlem3  28665  heiborlem5  28667  heiborlem10  28672  rrnequiv  28687  eldiophb  29048  4rexfrabdioph  29089  6rexfrabdioph  29090  diophren  29105  rencldnfilem  29112  pellexlem3  29125  pellfundglb  29179  rmxypairf1o  29205  rmxycomplete  29211  rmxyneg  29214  rmxyadd  29215  rmxy1  29216  rmxy0  29217  monotuz  29235  jm2.22  29297  aomclem2  29361  isnumbasgrp  29416  dfacbasgrp  29417  hbtlem2  29433  hbt  29439  elmnc  29446  issdrg  29507  cntzsdrg  29512  mon1psubm  29527  stoweidlem26  29774  stoweidlem51  29799  ige2m1fz  30159  psrass23l  30763  ply1ass23l  30767  suctrALT  31449  suctrALT3  31547  chordthmALT  31556  iunconlem2  31558  bnj1213  31679  bnj1417  31919  osumcllem7N  33446  pexmidlem4N  33457