Theorem sseldi 3452

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

Syntax hints:   -> wi 4   e. wcel 1758   C_ wss 3426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440

This theorem is referenced by:  onfr  4856  sofld  5384  fvrn0  5811  riotacl  6166  riotasbc  6167  elmpt2cl  6404  ofrval  6430  opiota  6733  mpt2xopn0yelv  6830  mpt2xopxnop0  6832  tpostpos  6865  smores  6913  tz7.44-2  6963  omopthlem2  7195  f1opwfi  7716  supub  7810  suplub  7811  ordtypelem3  7835  ordtypelem4  7836  ordtypelem6  7838  ordtypelem7  7839  wemapsolem  7865  wemapso2OLD  7867  wemapso2lem  7868  unxpwdom2  7904  oemapvali  7993  wemapwe  8029  wemapweOLD  8030  oef1o  8031  oef1oOLD  8032  cnfcomlem  8033  cnfcomlemOLD  8041  r1pwss  8092  r1elwf  8104  rankr1ai  8106  r0weon  8280  infxpenlem  8281  acnlem  8319  acndom2  8325  infpwfien  8333  alephfp  8379  ackbij1b  8509  cflim2  8533  fin23lem26  8595  isf32lem5  8627  isf32lem7  8629  isf32lem8  8630  isf32lem9  8631  isfin1-3  8656  fin1a2lem9  8678  fin1a2lem11  8680  hsmexlem5  8700  zorn2lem3  8768  zorn2lem4  8769  zorn2lem5  8770  ttukeylem6  8784  ttukeylem7  8785  iundom2g  8805  fpwwe2lem12  8909  pwfseqlem3  8928  gch2  8943  wunom  8988  rexrd  9534  nnred  10438  nncnd  10439  un0addcl  10714  un0mulcl  10715  nnnn0d  10737  nn0red  10738  suprzcl  10822  nn0zd  10846  zred  10848  zsupss  11045  rpnnen1lem1  11080  rpnnen1lem2  11081  rpred  11128  supicclub2  11537  zmodfzp1  11832  fzfi  11895  seqf1olem1  11946  expcl2lem  11978  m1expcl  11989  hashxrcl  12228  seqcoll2  12319  swrdspsleq  12444  wrdeqcats1  12470  wrdind  12473  wrd2ind  12474  limsupgre  13061  rlimpm  13080  rlimclim  13126  isercolllem1  13244  isercolllem2  13245  isercoll  13247  iseraltlem2  13262  iseraltlem3  13263  zsum  13297  fsumcvg3  13308  ackbijnn  13393  bitsval  13722  bitsfzolem  13732  bitsinv1  13740  smuval2  13780  gcdcllem3  13799  eulerthlem2  13959  prmdivdiv  13964  prmreclem1  14079  prmreclem2  14080  prmreclem3  14081  1arith  14090  4sqlem13  14120  4sqlem14  14121  4sqlem17  14124  vdwlem5  14148  vdwlem8  14151  vdwlem12  14155  vdwnnlem3  14160  ramtlecl  14163  ramcl2lem  14172  ramcl2  14179  ramxrcl  14180  submrc  14668  mreexexlem2d  14685  catlid  14723  catrid  14724  sscpwex  14830  subcrcl  14831  sscres  14838  wunfunc  14911  funcres2c  14913  cofull  14946  cofth  14947  coffth  14948  rescfth  14949  homarel  15006  arwrcl  15014  idaf  15033  homdmcoa  15037  coaval  15038  coapm  15041  catciso  15077  catcoppccl  15078  catcfuccl  15079  catcxpccl  15119  acsfiindd  15449  psssdm2  15487  submrcl  15576  gsumval2  15615  issubg  15783  isnsg  15812  nmzsubg  15824  conjnmz  15882  conjnmzb  15883  cntzsubm  15955  cntzsubg  15956  symggen  16078  symgtrinv  16080  psgnunilem5  16102  psgnunilem2  16103  psgnuni  16107  odlem2  16146  gexlem2  16185  sylow1lem2  16202  sylow1lem4  16204  sylow2a  16222  efglem  16317  efgtf  16323  efgtlen  16327  efgsres  16339  efgsfo  16340  efgredlemg  16343  efgredleme  16344  efgredlemd  16345  efgredlemc  16346  efgredlem  16348  efgred  16349  efgcpbllemb  16356  frgpuplem  16373  frgpnabllem2  16456  cyggex2  16477  dprdfsub  16616  dprdf11  16618  dprdfsubOLD  16623  dprdf11OLD  16625  dprd2da  16646  ablfac2  16695  issubrg  16971  cntzsubr  17003  abvrcl  17012  lbsextlem3  17347  sralmod  17374  rrgeq0  17467  psrbagconf1o  17550  psrass1lem  17553  psrdi  17585  psrdir  17586  psrass23l  17587  psrass23  17589  resspsrmul  17596  mplelf  17616  mplsubrglem  17624  mplsubrglemOLD  17625  mpladd  17628  mplmul  17629  mplvsca  17633  mplmonmul  17650  mplcoe5  17655  mplcoe2OLD  17657  mplind  17691  psropprmul  17800  ply1frcl  17862  nn0srg  17990  rge0srg  17991  zringlpirlem2  18013  zringlpirlem3  18014  zlpirlem2  18018  zlpirlem3  18019  znf1o  18093  cygznlem2a  18109  psgninv  18121  ocvlss  18206  lsmcss  18226  isobs  18254  mdetralt  18530  neiptoptop  18851  restbas  18878  ordtbas2  18911  ordtopn1  18914  ordtopn2  18915  ordtrest  18922  iocpnfordt  18935  icomnfordt  18936  lmrcl  18951  subbascn  18974  lmss  19018  cnconn  19142  clscon  19150  concompclo  19155  subislly  19201  cldllycmp  19215  kgeni  19226  llycmpkgen2  19239  1stckgenlem  19242  ptbasfi  19270  xkoopn  19278  txcls  19293  dfac14lem  19306  txcnp  19309  ptcnplem  19310  upxp  19312  txtube  19329  txcmplem1  19330  txcmplem2  19331  txkgen  19341  xkopt  19344  xkococnlem  19348  txcon  19378  basqtop  19400  tgqtop  19401  kqnrmlem1  19432  kqnrmlem2  19433  nrmhmph  19483  ptcmpfi  19502  elmptrab  19516  uzrest  19586  fclsfnflim  19716  flimfnfcls  19717  cnpfcf  19730  alexsubALTlem3  19737  alexsubALTlem4  19738  ptcmplem2  19741  ptcmplem5  19744  tsmsresOLD  19833  tsmsres  19834  restutop  19928  prdsxmetlem  20059  isxms2  20139  prdsbl  20182  met2ndci  20213  nmdvr  20367  nrginvrcnlem  20387  nrginvrcn  20388  tgqioo  20493  zdis  20509  reperflem  20511  reconnlem2  20520  reconn  20521  xrge0gsumle  20526  xrge0tsms  20527  xmetdcn  20531  metdcn  20533  metdscn2  20549  cncfmpt2ss  20607  icchmeo  20629  iccpnfcnv  20632  xrhmeo  20634  icccvx  20638  cnheibor  20643  bndth  20646  evth  20647  lebnum  20652  isphtpc  20682  reparphti  20685  pcoass  20712  nmoleub2lem  20785  nmoleub2lem3  20786  nmoleub2lem2  20787  nmoleub3  20790  nmhmcn  20791  cfili  20895  cfilfcls  20901  caussi  20924  equivcau  20927  rrxf  21016  minveclem4b  21034  minveclem4  21035  evthicc2  21060  ovolfcl  21066  ovolfioo  21067  ovolficc  21068  ovolficcss  21069  ovolfsval  21070  ovolmge0  21076  ovollb2lem  21087  ovolunlem1a  21095  ovoliunlem1  21101  ovolicc1  21115  ovolicc2lem4  21119  ovolicc2lem5  21120  ioombl1lem2  21156  ioombl1lem4  21158  ovolfs2  21167  ioorcl  21173  uniiccdif  21174  uniioovol  21175  uniiccvol  21176  uniioombllem2a  21178  uniioombllem2  21179  uniioombllem3a  21180  uniioombllem3  21181  uniioombllem4  21182  uniioombllem5  21183  uniioombllem6  21184  dyadmbl  21196  volsup2  21201  volivth  21203  vitalilem1  21204  vitalilem2  21205  vitalilem4  21207  mbfimaopnlem  21249  cncombf  21252  cnmbf  21253  mbflimsup  21260  mbfi1fseqlem3  21311  mbfi1fseqlem4  21312  mbfi1fseqlem5  21313  itg2const2  21335  itg2lea  21338  itg2eqa  21339  itg2split  21343  itg2i1fseq  21349  itg2gt0  21354  limcco  21484  dvcl  21490  perfdvf  21494  dvreslem  21500  dvres2lem  21501  dvidlem  21506  dvcnp2  21510  dvmulbr  21529  dvferm1lem  21572  dvferm2lem  21574  dvferm  21576  rolle  21578  dvlipcn  21582  dvlip2  21583  c1liplem1  21584  c1lip2  21586  dvgt0lem1  21590  dvivthlem1  21596  dvivth  21598  lhop1lem  21601  lhop1  21602  lhop2  21603  lhop  21604  dvfsumlem1  21614  dvfsumlem2  21615  dvfsumlem3  21616  dvfsumlem4  21617  dvfsumrlimge0  21618  dvfsumrlim  21619  dvfsumrlim2  21620  dvfsum2  21622  ftc1lem5  21628  ftc1lem6  21629  itgsubstlem  21636  itgsubst  21637  mdegleb  21651  mdegaddle  21661  mdegvsca  21663  mdegmullem  21665  ig1peu  21759  plybss  21778  plyaddcl  21804  plymulcl  21805  plysubcl  21806  coeidlem  21821  coesub  21840  dgrmulc  21854  dgrcolem1  21856  dgrcolem2  21857  dgrco  21858  quotlem  21882  quotcl2  21884  quotdgr  21885  plyrem  21887  facth  21888  quotcan  21891  vieta1lem1  21892  vieta1  21894  elqaalem3  21903  aalioulem2  21915  aalioulem3  21916  taylfvallem1  21938  tayl0  21943  dvntaylp  21952  taylthlem1  21954  taylthlem2  21955  radcnvlt1  21999  radcnvle  22001  pserulm  22003  psercnlem2  22005  psercnlem1  22006  psercn  22007  pserdvlem1  22008  pserdvlem2  22009  abelthlem3  22014  abelthlem5  22016  abelthlem6  22017  abelth  22022  efcvx  22030  tanord  22110  tanregt0  22111  efif1olem4  22117  logtayl  22221  logccv  22224  cxpcn3  22302  ssscongptld  22336  chordthmlem  22343  chordthmlem4  22346  chordthmlem5  22347  chordthm  22348  heron  22349  asinrecl  22413  atantan  22434  dvatan  22446  leibpi  22453  rlimcnp  22475  efrlim  22479  cvxcl  22494  scvxcvx  22495  jensenlem1  22496  jensenlem2  22497  jensen  22498  amgmlem  22499  harmonicbnd3  22517  wilthlem1  22522  ftalem3  22528  ftalem5  22530  ftalem7  22532  basellem3  22536  basellem4  22537  basellem5  22538  ppisval  22557  chtf  22562  efchtcl  22565  chtge0  22566  sgmval2  22597  ppinprm  22606  chtprm  22607  chtnprm  22608  chtwordi  22610  chtdif  22612  efchtdvds  22613  sqff1o  22636  fsumdvdsdiaglem  22639  fsumdvdsdiag  22640  fsumdvdscom  22641  musum  22647  muinv  22649  dvdsmulf1o  22650  sgmmul  22656  chtlepsi  22661  chtleppi  22665  pclogsum  22670  chpval2  22673  chpchtsum  22674  chpub  22675  perfectlem2  22685  dchrelbasd  22694  dchrrcl  22695  dchrzrh1  22699  dchrzrhmul  22701  dchrinvcl  22708  dchrfi  22710  dchrghm  22711  dchr1  22712  dchrabs  22715  dchrinv  22716  dchrptlem2  22720  dchrsum2  22723  sumdchr2  22725  sum2dchr  22729  lgscl  22765  lgsquadlem1  22809  lgsquadlem2  22810  2sqlem6  22824  2sqlem8  22827  2sqlem9  22828  chebbnd1lem1  22834  chtppilimlem1  22838  rplogsumlem2  22850  dchrisum0flblem1  22873  rpvmasum2  22877  dchrisum0re  22878  dchrisum0lema  22879  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0lem2  22883  dchrisum0lem3  22884  dchrisum0  22885  rplogsum  22892  dirith2  22893  mudivsum  22895  mulogsum  22897  mulog2sumlem2  22900  vmalogdivsum2  22903  logsqvma  22907  logsqvma2  22908  selberglem3  22912  selberg  22913  chpdifbndlem1  22918  selberg34r  22936  pntsval2  22941  pntrlog2bndlem1  22942  pntpbnd1a  22950  pntpbnd1  22951  pntpbnd2  22952  pntibndlem2a  22955  pntibndlem2  22956  pntibndlem3  22957  pntlemd  22959  padicabv  22995  axtgcgrrflx  23039  axtgcgrid  23040  axtgsegcon  23041  axtg5seg  23042  axtgbtwnid  23043  axtgpasch  23044  axtgcont1  23045  perpcom  23232  perpneq  23233  ragperp  23236  ttgcontlem1  23266  axlowdimlem16  23338  axcontlem10  23354  umgrass  23388  umgran0  23389  usgrass  23418  redwlk  23640  issubgo  23925  nvvop  24122  nmcnc  24226  ubthlem1  24406  minvecolem2  24411  minvecolem3  24412  minvecolem5  24417  minvecolem6  24418  minvecolem7  24419  hlimcaui  24774  pjocini  25236  fcnvgreu  26125  f1od2  26158  xrge0infss  26187  xrge0infssd  26188  eliccelico  26201  elicoelioo  26202  iundisjfi  26214  iundisj2fi  26215  divnumden2  26221  xrsmulgzz  26273  ressmulgnn  26278  ressmulgnn0  26279  xrge0addass  26285  xrge0addgt0  26288  xrge0adddir  26289  xrge0adddi  26290  xrge0npcan  26291  fsumrp0cl  26292  archirngz  26340  archiabllem1b  26343  gsummpt2co  26383  regsumfsum  26384  xrge0tsmsd  26387  dvrdir  26392  rdivmuldivd  26393  dvrcan5  26395  elrhmunit  26422  rhmunitinv  26424  xrge0slmod  26446  cnre2csqima  26475  tpr2rico  26476  cnvordtrestixx  26477  ordtrestNEW  26485  xrge0iifcnv  26497  xrge0iifhom  26501  xrge0mulc1cn  26505  rge0scvg  26513  lmxrge0  26516  cnzh  26533  rezh  26534  qqhval2  26545  qqhvq  26550  qqhnm  26553  qqhcn  26554  qqhucn  26555  indsum  26613  indf1ofs  26616  esumel  26635  esumle  26642  esummono  26643  gsumesum  26644  esumlub  26645  esumlef  26647  esumcst  26648  esumfzf  26652  esumfsup  26653  esumfsupre  26654  esumpinfval  26656  esumpfinvallem  26657  esumpfinval  26658  esumpfinvalf  26659  esumpinfsum  26660  esumpcvgval  26661  esumpmono  26662  esummulc1  26664  esummulc2  26665  esumdivc  26666  hasheuni  26668  esumcvg  26669  sigainb  26713  measun  26759  measunl  26764  measiun  26766  meascnbl  26767  voliune  26779  volfiniune  26780  ddemeas  26786  dya2icoseg2  26827  dya2iocnrect  26830  sxbrsigalem2  26835  oms0  26844  omsmon  26845  sibfof  26860  oddpwdc  26871  eulerpartlemgc  26879  eulerpartlemgvv  26893  eulerpartlemgf  26896  eulerpartlemgs2  26897  eulerpartlemn  26898  sseqf  26909  probun  26936  probdif  26937  probvalrnd  26941  probmeasb  26947  cndprobin  26951  bayesth  26956  ballotlemsdom  27028  ballotlemrv2  27038  ballotlemfrci  27044  sgnclre  27056  plymulx0  27082  signsply0  27086  signswch  27096  signstf  27101  signsvtn0  27105  signsvfn  27117  signlem0  27122  lgamgulmlem2  27150  lgamcvg2  27175  subfacp1lem5  27206  erdszelem4  27216  erdszelem6  27218  erdszelem7  27219  erdszelem8  27220  erdszelem9  27221  conpcon  27258  cvxscon  27266  rescon  27269  iccllyscon  27273  rellyscon  27274  cvmsrcl  27287  cvmliftmolem2  27305  cvmlift2lem12  27337  cvmlift3  27351  snmlval  27354  clim2prod  27537  ntrivcvg  27546  ntrivcvgfvn0  27548  ntrivcvgtail  27549  ntrivcvgmullem  27550  ntrivcvgmul  27551  prodrblem  27576  prodmolem2a  27581  mblfinlem2  28567  itg2addnclem3  28583  itg2addnc  28584  itg2gt0cn  28585  ftc1cnnclem  28603  ftc1anclem6  28610  islocfin  28706  neibastop1  28718  fdc  28779  prdsbnd  28830  ismtyval  28837  heiborlem3  28850  heiborlem5  28852  heiborlem10  28857  rrnequiv  28872  eldiophb  29233  4rexfrabdioph  29274  6rexfrabdioph  29275  diophren  29290  rencldnfilem  29297  pellexlem3  29310  pellfundglb  29364  rmxypairf1o  29390  rmxycomplete  29396  rmxyneg  29399  rmxyadd  29400  rmxy1  29401  rmxy0  29402  monotuz  29420  jm2.22  29482  aomclem2  29546  isnumbasgrp  29601  dfacbasgrp  29602  hbtlem2  29618  hbt  29624  elmnc  29631  issdrg  29692  cntzsdrg  29697  mon1psubm  29712  stoweidlem26  29959  stoweidlem51  29984  ige2m1fz  30344  ply1ass23l  30970  suctrALT  31862  suctrALT3  31960  chordthmALT  31969  iunconlem2  31971  bnj1213  32092  bnj1417  32332  osumcllem7N  33912  pexmidlem4N  33923