Theorem sseldi 3415

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

Syntax hints:   -> wi 4   e. wcel 1826   C_ wss 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3396  df-ss 3403

This theorem is referenced by:  onfr  4831  sofld  5364  fvrn0  5796  riotacl  6172  riotasbc  6173  ovima0  6353  elmpt2cl  6416  ofrval  6449  opiota  6758  mpt2xopn0yelv  6859  mpt2xopxnop0  6861  tpostpos  6893  smores  6941  tz7.44-2  6991  omopthlem2  7223  f1opwfi  7739  supub  7833  suplub  7834  ordtypelem3  7860  ordtypelem4  7861  ordtypelem6  7863  ordtypelem7  7864  wemapsolem  7890  wemapso2OLD  7892  wemapso2lem  7893  unxpwdom2  7929  oemapvali  8016  wemapwe  8052  wemapweOLD  8053  oef1o  8054  oef1oOLD  8055  cnfcomlem  8056  cnfcomlemOLD  8064  r1pwss  8115  r1elwf  8127  rankr1ai  8129  r0weon  8303  infxpenlem  8304  acnlem  8342  acndom2  8348  infpwfien  8356  alephfp  8402  ackbij1b  8532  cflim2  8556  fin23lem26  8618  isf32lem5  8650  isf32lem7  8652  isf32lem8  8653  isf32lem9  8654  isfin1-3  8679  fin1a2lem9  8701  fin1a2lem11  8703  hsmexlem5  8723  zorn2lem3  8791  zorn2lem4  8792  zorn2lem5  8793  ttukeylem6  8807  ttukeylem7  8808  iundom2g  8828  fpwwe2lem12  8930  pwfseqlem3  8949  gch2  8964  wunom  9009  rexrd  9554  nnred  10467  nncnd  10468  un0addcl  10746  un0mulcl  10747  nnnn0d  10769  nn0red  10770  suprzcl  10859  nn0zd  10882  zred  10884  zsupss  11090  rpnnen1lem1  11127  rpnnen1lem2  11128  rpred  11177  supicclub2  11592  ige2m1fz  11690  zmodfzp1  11920  fzfi  11985  seqf1olem1  12049  expcl2lem  12081  m1expcl  12092  hashxrcl  12331  seqcoll2  12417  ccatrn  12515  wrdeqcats1OLD  12610  wrdind  12613  wrd2ind  12614  cotr2g  12814  limsupgre  13306  rlimpm  13325  rlimclim  13371  isercolllem1  13489  isercolllem2  13490  isercoll  13492  iseraltlem2  13507  iseraltlem3  13508  zsum  13542  fsumcvg3  13553  ackbijnn  13642  clim2prod  13699  ntrivcvg  13708  ntrivcvgfvn0  13710  ntrivcvgtail  13711  ntrivcvgmullem  13712  ntrivcvgmul  13713  prodrblem  13738  prodmolem2a  13743  bitsval  14076  bitsfzolem  14086  bitsinv1  14094  smuval2  14134  gcdcllem3  14153  eulerthlem2  14314  prmdivdiv  14319  prmreclem1  14436  prmreclem2  14437  prmreclem3  14438  1arith  14447  4sqlem13  14477  4sqlem14  14478  4sqlem17  14481  vdwlem5  14505  vdwlem8  14508  vdwlem12  14512  vdwnnlem3  14517  ramtlecl  14520  ramcl2lem  14529  ramcl2  14536  ramxrcl  14537  submrc  15035  mreexexlem2d  15052  catlid  15090  catrid  15091  sscpwex  15221  subcrcl  15222  sscres  15229  wunfunc  15305  funcres2c  15307  cofull  15340  cofth  15341  coffth  15342  rescfth  15343  homarel  15432  arwrcl  15440  idaf  15459  homdmcoa  15463  coaval  15464  coapm  15467  catciso  15503  catcoppccl  15504  catcfuccl  15505  catcxpccl  15593  acsfiindd  15924  psssdm2  15962  gsumval2  16024  submrcl  16094  issubg  16318  isnsg  16347  nmzsubg  16359  conjnmz  16417  conjnmzb  16418  cntzsubm  16490  cntzsubg  16491  symggen  16612  symgtrinv  16614  psgnunilem5  16636  psgnunilem2  16637  psgnuni  16641  odlem2  16680  gexlem2  16719  sylow1lem2  16736  sylow1lem4  16738  sylow2a  16756  efglem  16851  efgtf  16857  efgtlen  16861  efgsres  16873  efgsfo  16874  efgredlemg  16877  efgredleme  16878  efgredlemd  16879  efgredlemc  16880  efgredlem  16882  efgred  16883  efgcpbllemb  16890  frgpuplem  16907  frgpnabllem2  16995  cyggex2  17016  dprdfsub  17174  dprdf11  17176  dprdfsubOLD  17181  dprdf11OLD  17183  dprd2da  17204  ablfac2  17253  issubrg  17542  cntzsubr  17574  abvrcl  17583  lbsextlem3  17919  sralmod  17946  rrgeq0  18051  psrbagconf1o  18139  psrass1lem  18142  psrdi  18174  psrdir  18175  psrass23l  18176  psrass23  18178  resspsrmul  18185  mplelf  18205  mplsubrglem  18213  mplsubrglemOLD  18214  mpladd  18217  mplmul  18218  mplvsca  18222  mplmonmul  18239  mplcoe5  18244  mplcoe2OLD  18246  mplind  18280  psropprmul  18392  ply1frcl  18468  rge0srg  18600  zringlpirlem2  18616  zringlpirlem3  18617  znf1o  18681  cygznlem2a  18697  psgninv  18709  ocvlss  18794  lsmcss  18814  isobs  18842  mdetralt  19195  neiptoptop  19718  restbas  19745  ordtbas2  19778  ordtopn1  19781  ordtopn2  19782  ordtrest  19789  iocpnfordt  19802  icomnfordt  19803  lmrcl  19818  subbascn  19841  lmss  19885  cnconn  20008  clscon  20016  concompclo  20021  subislly  20067  cldllycmp  20081  islocfin  20103  kgeni  20123  llycmpkgen2  20136  1stckgenlem  20139  ptbasfi  20167  xkoopn  20175  txcls  20190  dfac14lem  20203  txcnp  20206  ptcnplem  20207  upxp  20209  txtube  20226  txcmplem1  20227  txcmplem2  20228  txkgen  20238  xkopt  20241  xkococnlem  20245  txcon  20275  basqtop  20297  tgqtop  20298  kqnrmlem1  20329  kqnrmlem2  20330  nrmhmph  20380  ptcmpfi  20399  elmptrab  20413  uzrest  20483  fclsfnflim  20613  flimfnfcls  20614  cnpfcf  20627  alexsubALTlem3  20634  alexsubALTlem4  20635  ptcmplem2  20638  ptcmplem5  20641  tsmsresOLD  20730  tsmsres  20731  restutop  20825  prdsxmetlem  20956  isxms2  21036  prdsbl  21079  met2ndci  21110  nmdvr  21264  nrginvrcnlem  21284  nrginvrcn  21285  tgqioo  21390  zdis  21406  reperflem  21408  reconnlem2  21417  reconn  21418  xrge0gsumle  21423  xrge0tsms  21424  xmetdcn  21428  metdcn  21430  metdscn2  21446  cncfmpt2ss  21504  icchmeo  21526  iccpnfcnv  21529  xrhmeo  21531  icccvx  21535  cnheibor  21540  bndth  21543  evth  21544  lebnum  21549  isphtpc  21579  reparphti  21582  pcoass  21609  nmoleub2lem  21682  nmoleub2lem3  21683  nmoleub2lem2  21684  nmoleub3  21687  nmhmcn  21688  cfili  21792  cfilfcls  21798  caussi  21821  equivcau  21824  rrxf  21913  minveclem4b  21931  minveclem4  21932  evthicc2  21957  ovolfcl  21963  ovolfioo  21964  ovolficc  21965  ovolficcss  21966  ovolfsval  21967  ovolmge0  21973  ovollb2lem  21984  ovolunlem1a  21992  ovoliunlem1  21998  ovolicc1  22012  ovolicc2lem4  22016  ovolicc2lem5  22017  ioombl1lem2  22054  ioombl1lem4  22056  ovolfs2  22065  ioorcl  22071  uniiccdif  22072  uniioovol  22073  uniiccvol  22074  uniioombllem2a  22076  uniioombllem2  22077  uniioombllem3a  22078  uniioombllem3  22079  uniioombllem4  22080  uniioombllem5  22081  uniioombllem6  22082  dyadmbl  22094  volsup2  22099  volivth  22101  vitalilem1  22102  vitalilem2  22103  vitalilem4  22105  mbfimaopnlem  22147  cncombf  22150  cnmbf  22151  mbflimsup  22158  mbfi1fseqlem3  22209  mbfi1fseqlem4  22210  mbfi1fseqlem5  22211  itg2const2  22233  itg2lea  22236  itg2eqa  22237  itg2split  22241  itg2i1fseq  22247  itg2gt0  22252  limcco  22382  dvcl  22388  perfdvf  22392  dvreslem  22398  dvres2lem  22399  dvidlem  22404  dvcnp2  22408  dvmulbr  22427  dvferm1lem  22470  dvferm2lem  22472  dvferm  22474  rolle  22476  dvlipcn  22480  dvlip2  22481  c1liplem1  22482  c1lip2  22484  dvgt0lem1  22488  dvivthlem1  22494  dvivth  22496  lhop1lem  22499  lhop1  22500  lhop2  22501  lhop  22502  dvfsumlem1  22512  dvfsumlem2  22513  dvfsumlem3  22514  dvfsumlem4  22515  dvfsumrlimge0  22516  dvfsumrlim  22517  dvfsumrlim2  22518  dvfsum2  22520  ftc1lem5  22526  ftc1lem6  22527  itgsubstlem  22534  itgsubst  22535  mdegleb  22549  mdegaddle  22559  mdegvsca  22561  mdegmullem  22563  ig1peu  22657  plybss  22676  plyaddcl  22702  plymulcl  22703  plysubcl  22704  coeidlem  22719  coesub  22739  dgrmulc  22753  dgrcolem1  22755  dgrcolem2  22756  dgrco  22757  quotlem  22781  quotcl2  22783  quotdgr  22784  plyrem  22786  facth  22787  quotcan  22790  vieta1lem1  22791  vieta1  22793  elqaalem3  22802  aalioulem2  22814  aalioulem3  22815  taylfvallem1  22837  tayl0  22842  dvntaylp  22851  taylthlem1  22853  taylthlem2  22854  radcnvlt1  22898  radcnvle  22900  pserulm  22902  psercnlem2  22904  psercnlem1  22905  psercn  22906  pserdvlem1  22907  pserdvlem2  22908  abelthlem3  22913  abelthlem5  22915  abelthlem6  22916  abelth  22921  efcvx  22929  tanord  23010  tanregt0  23011  efif1olem4  23017  logtayl  23128  logccv  23131  cxpcn3  23209  ssscongptld  23272  chordthmlem  23279  chordthmlem4  23282  chordthmlem5  23283  chordthm  23284  heron  23285  asinrecl  23349  atantan  23370  dvatan  23382  leibpi  23389  rlimcnp  23412  efrlim  23416  cvxcl  23431  scvxcvx  23432  jensenlem1  23433  jensenlem2  23434  jensen  23435  amgmlem  23436  harmonicbnd3  23454  wilthlem1  23459  ftalem3  23465  ftalem5  23467  ftalem7  23469  basellem3  23473  basellem4  23474  basellem5  23475  ppisval  23494  chtf  23499  efchtcl  23502  chtge0  23503  sgmval2  23534  ppinprm  23543  chtprm  23544  chtnprm  23545  chtwordi  23547  chtdif  23549  efchtdvds  23550  sqff1o  23573  fsumdvdsdiaglem  23576  fsumdvdsdiag  23577  fsumdvdscom  23578  musum  23584  muinv  23586  dvdsmulf1o  23587  sgmmul  23593  chtlepsi  23598  chtleppi  23602  pclogsum  23607  chpval2  23610  chpchtsum  23611  chpub  23612  perfectlem2  23622  dchrelbasd  23631  dchrrcl  23632  dchrzrh1  23636  dchrzrhmul  23638  dchrinvcl  23645  dchrfi  23647  dchrghm  23648  dchr1  23649  dchrabs  23652  dchrinv  23653  dchrptlem2  23657  dchrsum2  23660  sumdchr2  23662  sum2dchr  23666  lgscl  23702  lgsquadlem1  23746  lgsquadlem2  23747  2sqlem6  23761  2sqlem8  23764  2sqlem9  23765  chebbnd1lem1  23771  chtppilimlem1  23775  rplogsumlem2  23787  dchrisum0flblem1  23810  rpvmasum2  23814  dchrisum0re  23815  dchrisum0lema  23816  dchrisum0lem1b  23817  dchrisum0lem1  23818  dchrisum0lem2a  23819  dchrisum0lem2  23820  dchrisum0lem3  23821  dchrisum0  23822  rplogsum  23829  dirith2  23830  mudivsum  23832  mulogsum  23834  mulog2sumlem2  23837  vmalogdivsum2  23840  logsqvma  23844  logsqvma2  23845  selberglem3  23849  selberg  23850  chpdifbndlem1  23855  selberg34r  23873  pntsval2  23878  pntrlog2bndlem1  23879  pntpbnd1a  23887  pntpbnd1  23888  pntpbnd2  23889  pntibndlem2a  23892  pntibndlem2  23893  pntibndlem3  23894  pntlemd  23896  padicabv  23932  axtgcgrrflx  23976  axtgcgrid  23977  axtgsegcon  23978  axtg5seg  23979  axtgbtwnid  23980  axtgpasch  23981  axtgcont1  23982  perpcom  24210  perpneq  24211  ragperp  24214  ttgcontlem1  24309  axlowdimlem16  24381  axcontlem10  24397  umgrass  24440  umgran0  24441  usgrass  24482  redwlk  24729  issubgo  25422  nvvop  25619  nmcnc  25723  ubthlem1  25903  minvecolem2  25908  minvecolem3  25909  minvecolem5  25914  minvecolem6  25915  minvecolem7  25916  hlimcaui  26271  pjocini  26733  fcnvgreu  27660  f1od2  27697  xrge0infss  27730  xrge0infssd  27731  xrge0subcld  27733  eliccelico  27741  elicoelioo  27742  iundisjfi  27754  iundisj2fi  27755  divnumden2  27762  xrsmulgzz  27819  ressmulgnn  27824  ressmulgnn0  27825  xrge0addass  27831  xrge0addgt0  27834  xrge0adddir  27835  xrge0adddi  27836  xrge0npcan  27837  fsumrp0cl  27838  gsummpt2co  27924  xrge0tsmsd  27929  dvrdir  27934  rdivmuldivd  27935  dvrcan5  27937  elrhmunit  27964  rhmunitinv  27966  xrge0slmod  27988  cnre2csqima  28047  tpr2rico  28048  cnvordtrestixx  28049  ordtrestNEW  28057  xrge0iifcnv  28069  xrge0iifhom  28073  xrge0mulc1cn  28077  rge0scvg  28085  lmxrge0  28088  qqhval2  28116  qqhvq  28121  qqhnm  28124  qqhcn  28125  qqhucn  28126  indsum  28171  indf1ofs  28174  esumel  28195  esummono  28202  esumpad  28203  esumpad2  28204  esumle  28206  gsumesum  28207  esumlub  28208  esumlef  28210  esumcst  28211  esumrnmpt2  28216  esumfzf  28217  esumfsup  28218  esumfsupre  28219  esumpinfval  28221  esumpfinvallem  28222  esumpfinval  28223  esumpfinvalf  28224  esumpinfsum  28225  esumpcvgval  28226  esumpmono  28227  esummulc1  28229  esummulc2  28230  esumdivc  28231  hasheuni  28233  esumcvg  28234  esumcvgsum  28236  esumgect  28238  esum2dlem  28240  esum2d  28241  sigainb  28285  measun  28338  measunl  28343  measiun  28345  meascnbl  28346  voliune  28357  volfiniune  28358  ddemeas  28364  dya2icoseg2  28405  dya2iocnrect  28408  sxbrsigalem2  28413  omscl  28422  oms0  28424  omsmon  28425  omssubadd  28427  baselcarsg  28433  0elcarsg  28434  difelcarsg  28437  inelcarsg  28438  carsgsigalem  28442  carsggect  28445  carsgclctunlem2  28446  carsgclctunlem3  28447  carsgclctun  28448  omsmeas  28450  sibfof  28465  oddpwdc  28476  eulerpartlemgc  28484  eulerpartlemgvv  28498  eulerpartlemgf  28501  eulerpartlemgs2  28502  eulerpartlemn  28503  sseqf  28514  probun  28541  probdif  28542  probvalrnd  28546  probmeasb  28552  cndprobin  28556  bayesth  28561  ballotlemsdom  28633  ballotlemrv2  28643  ballotlemfrci  28649  sgnclre  28661  signswch  28701  signstf  28706  signsvtn0  28710  signsvfn  28722  signlem0  28727  lgamgulmlem2  28761  lgamcvg2  28786  subfacp1lem5  28817  erdszelem4  28827  erdszelem6  28829  erdszelem7  28830  erdszelem8  28831  erdszelem9  28832  conpcon  28869  cvxscon  28877  rescon  28880  iccllyscon  28884  rellyscon  28885  cvmsrcl  28898  cvmliftmolem2  28916  cvmlift2lem12  28948  cvmlift3  28962  snmlval  28965  mrsubvr  29060  msubff1  29105  mclsax  29118  mthmpps  29131  mclspps  29133  mblfinlem2  30217  itg2addnclem3  30234  itg2addnc  30235  itg2gt0cn  30236  ftc1cnnclem  30254  ftc1anclem6  30261  neibastop1  30343  fdc  30404  prdsbnd  30455  ismtyval  30462  heiborlem3  30475  heiborlem5  30477  heiborlem10  30482  rrnequiv  30497  eldiophb  30855  4rexfrabdioph  30897  6rexfrabdioph  30898  diophren  30912  rencldnfilem  30919  pellexlem3  30932  pellfundglb  30986  rmxypairf1o  31012  rmxycomplete  31018  rmxyneg  31021  rmxyadd  31022  rmxy1  31023  rmxy0  31024  monotuz  31042  jm2.22  31103  aomclem2  31167  isnumbasgrp  31224  dfacbasgrp  31225  hbtlem2  31241  hbt  31247  elmnc  31253  issdrg  31314  cntzsdrg  31319  mon1psubm  31334  lcmn0cl  31371  hashnzfz2  31394  evthiccabs  31695  mullimc  31788  limccog  31792  mullimcf  31795  limcperiod  31800  limcrecl  31801  sumnnodd  31802  ltmod  31810  limcresiooub  31814  limcresioolb  31815  limcleqr  31816  neglimc  31819  addlimc  31820  limclner  31823  sublimc  31824  reclimc  31825  limclr  31827  divlimc  31828  cncficcgt0  31857  cncfiooicclem1  31862  cncfiooicc  31863  cncfiooiccre  31864  cncfioobdlem  31865  cncfioobd  31866  fperdvper  31881  dvbdfbdioolem1  31891  ioodvbdlimc1lem1  31894  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  dvdmsscn  31899  dvnmptconst  31904  dvnxpaek  31905  dvnmul  31906  dvnprodlem3  31911  itgsincmulx  31939  itgioocnicc  31942  iblcncfioo  31943  stoweidlem26  31974  stoweidlem51  31999  dirkercncflem2  32052  fourierdlem1  32056  fourierdlem16  32071  fourierdlem18  32073  fourierdlem19  32074  fourierdlem20  32075  fourierdlem21  32076  fourierdlem22  32077  fourierdlem24  32079  fourierdlem25  32080  fourierdlem27  32082  fourierdlem31  32086  fourierdlem32  32087  fourierdlem33  32088  fourierdlem35  32090  fourierdlem37  32092  fourierdlem39  32094  fourierdlem41  32096  fourierdlem42  32097  fourierdlem46  32101  fourierdlem51  32106  fourierdlem60  32115  fourierdlem61  32116  fourierdlem62  32117  fourierdlem64  32119  fourierdlem65  32120  fourierdlem66  32121  fourierdlem68  32123  fourierdlem71  32126  fourierdlem73  32128  fourierdlem74  32129  fourierdlem75  32130  fourierdlem76  32131  fourierdlem78  32133  fourierdlem79  32134  fourierdlem81  32136  fourierdlem82  32137  fourierdlem83  32138  fourierdlem84  32139  fourierdlem85  32140  fourierdlem87  32142  fourierdlem88  32143  fourierdlem89  32144  fourierdlem91  32146  fourierdlem95  32150  fourierdlem101  32156  fourierdlem102  32157  fourierdlem103  32158  fourierdlem104  32159  fourierdlem111  32166  fourierdlem112  32167  fourierdlem114  32169  fouriercnp  32175  fouriersw  32180  fouriercn  32181  elaa2lem  32182  elaa2  32183  etransclem14  32197  etransclem15  32198  etransclem24  32207  etransclem25  32208  etransclem26  32209  etransclem31  32214  etransclem32  32215  etransclem33  32216  etransclem34  32217  etransclem35  32218  etransclem38  32221  etransclem44  32227  etransclem48  32231  perfectALTVlem2  32544  submgmrcl  32788  inclfusubc  32873  ply1ass23l  33182  suctrALT  33972  suctrALT3  34071  chordthmALT  34080  iunconlem2  34082  bnj1213  34204  bnj1417  34444  osumcllem7N  36099  pexmidlem4N  36110  imo72b2  38522