Theorem sseldi 3342

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

Syntax hints:   -> wi 4   e. wcel 1755   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330

This theorem is referenced by:  onfr  4745  sofld  5274  fvrn0  5700  riotacl  6055  riotasbc  6056  elmpt2cl  6293  ofrval  6319  opiota  6622  mpt2xopn0yelv  6719  mpt2xopxnop0  6721  tpostpos  6754  smores  6799  tz7.44-2  6849  omopthlem2  7083  f1opwfi  7603  supub  7697  suplub  7698  ordtypelem3  7722  ordtypelem4  7723  ordtypelem6  7725  ordtypelem7  7726  wemapsolem  7752  wemapso2OLD  7754  wemapso2lem  7755  unxpwdom2  7791  oemapvali  7880  wemapwe  7916  wemapweOLD  7917  oef1o  7918  oef1oOLD  7919  cnfcomlem  7920  cnfcomlemOLD  7928  r1pwss  7979  r1elwf  7991  rankr1ai  7993  r0weon  8167  infxpenlem  8168  acnlem  8206  acndom2  8212  infpwfien  8220  alephfp  8266  ackbij1b  8396  cflim2  8420  fin23lem26  8482  isf32lem5  8514  isf32lem7  8516  isf32lem8  8517  isf32lem9  8518  isfin1-3  8543  fin1a2lem9  8565  fin1a2lem11  8567  hsmexlem5  8587  zorn2lem3  8655  zorn2lem4  8656  zorn2lem5  8657  ttukeylem6  8671  ttukeylem7  8672  iundom2g  8692  fpwwe2lem12  8796  pwfseqlem3  8815  gch2  8830  wunom  8875  rexrd  9421  nnred  10325  nncnd  10326  un0addcl  10601  un0mulcl  10602  nnnn0d  10624  nn0red  10625  suprzcl  10709  nn0zd  10733  zred  10735  zsupss  10932  rpnnen1lem1  10967  rpnnen1lem2  10968  rpred  11015  supicclub2  11423  zmodfzp1  11715  fzfi  11778  seqf1olem1  11829  expcl2lem  11861  m1expcl  11872  hashxrcl  12111  seqcoll2  12201  swrdspsleq  12326  wrdeqcats1  12352  wrdind  12355  wrd2ind  12356  limsupgre  12943  rlimpm  12962  rlimclim  13008  isercolllem1  13126  isercolllem2  13127  isercoll  13129  iseraltlem2  13144  iseraltlem3  13145  zsum  13179  fsumcvg3  13190  ackbijnn  13274  bitsval  13603  bitsfzolem  13613  bitsinv1  13621  smuval2  13661  gcdcllem3  13680  eulerthlem2  13840  prmdivdiv  13845  prmreclem1  13960  prmreclem2  13961  prmreclem3  13962  1arith  13971  4sqlem13  14001  4sqlem14  14002  4sqlem17  14005  vdwlem5  14029  vdwlem8  14032  vdwlem12  14036  vdwnnlem3  14041  ramtlecl  14044  ramcl2lem  14053  ramcl2  14060  ramxrcl  14061  submrc  14549  mreexexlem2d  14566  catlid  14604  catrid  14605  sscpwex  14711  subcrcl  14712  sscres  14719  wunfunc  14792  funcres2c  14794  cofull  14827  cofth  14828  coffth  14829  rescfth  14830  homarel  14887  arwrcl  14895  idaf  14914  homdmcoa  14918  coaval  14919  coapm  14922  catciso  14958  catcoppccl  14959  catcfuccl  14960  catcxpccl  15000  acsfiindd  15330  psssdm2  15368  submrcl  15456  gsumval2  15493  issubg  15661  isnsg  15690  nmzsubg  15702  conjnmz  15760  conjnmzb  15761  cntzsubm  15833  cntzsubg  15834  symggen  15956  symgtrinv  15958  psgnunilem5  15980  psgnunilem2  15981  psgnuni  15985  odlem2  16022  gexlem2  16061  sylow1lem2  16078  sylow1lem4  16080  sylow2a  16098  efglem  16193  efgtf  16199  efgtlen  16203  efgsres  16215  efgsfo  16216  efgredlemg  16219  efgredleme  16220  efgredlemd  16221  efgredlemc  16222  efgredlem  16224  efgred  16225  efgcpbllemb  16232  frgpuplem  16249  frgpnabllem2  16332  cyggex2  16353  dprdfsub  16485  dprdf11  16487  dprdfsubOLD  16492  dprdf11OLD  16494  dprd2da  16515  ablfac2  16564  issubrg  16789  cntzsubr  16821  abvrcl  16830  lbsextlem3  17163  sralmod  17190  rrgeq0  17283  psrbagconf1o  17378  psrass1lem  17381  psrdi  17413  psrdir  17414  psrass23  17416  resspsrmul  17423  mplelf  17443  mplsubrglem  17451  mplsubrglemOLD  17452  mpladd  17455  mplmul  17456  mplvsca  17460  mplmonmul  17477  mplcoe2  17481  mplcoe2OLD  17482  mplind  17516  psropprmul  17591  zringlpirlem2  17746  zringlpirlem3  17747  zlpirlem2  17751  zlpirlem3  17752  znf1o  17826  cygznlem2a  17842  psgninv  17854  ocvlss  17939  lsmcss  17959  isobs  17987  mdetralt  18256  neiptoptop  18577  restbas  18604  ordtbas2  18637  ordtopn1  18640  ordtopn2  18641  ordtrest  18648  iocpnfordt  18661  icomnfordt  18662  lmrcl  18677  subbascn  18700  lmss  18744  cnconn  18868  clscon  18876  concompclo  18881  subislly  18927  cldllycmp  18941  kgeni  18952  llycmpkgen2  18965  1stckgenlem  18968  ptbasfi  18996  xkoopn  19004  txcls  19019  dfac14lem  19032  txcnp  19035  ptcnplem  19036  upxp  19038  txtube  19055  txcmplem1  19056  txcmplem2  19057  txkgen  19067  xkopt  19070  xkococnlem  19074  txcon  19104  basqtop  19126  tgqtop  19127  kqnrmlem1  19158  kqnrmlem2  19159  nrmhmph  19209  ptcmpfi  19228  elmptrab  19242  uzrest  19312  fclsfnflim  19442  flimfnfcls  19443  cnpfcf  19456  alexsubALTlem3  19463  alexsubALTlem4  19464  ptcmplem2  19467  ptcmplem5  19470  tsmsresOLD  19559  tsmsres  19560  restutop  19654  prdsxmetlem  19785  isxms2  19865  prdsbl  19908  met2ndci  19939  nmdvr  20093  nrginvrcnlem  20113  nrginvrcn  20114  tgqioo  20219  zdis  20235  reperflem  20237  reconnlem2  20246  reconn  20247  xrge0gsumle  20252  xrge0tsms  20253  xmetdcn  20257  metdcn  20259  metdscn2  20275  cncfmpt2ss  20333  icchmeo  20355  iccpnfcnv  20358  xrhmeo  20360  icccvx  20364  cnheibor  20369  bndth  20372  evth  20373  lebnum  20378  isphtpc  20408  reparphti  20411  pcoass  20438  nmoleub2lem  20511  nmoleub2lem3  20512  nmoleub2lem2  20513  nmoleub3  20516  nmhmcn  20517  cfili  20621  cfilfcls  20627  caussi  20650  equivcau  20653  rrxf  20742  minveclem4b  20760  minveclem4  20761  evthicc2  20786  ovolfcl  20792  ovolfioo  20793  ovolficc  20794  ovolficcss  20795  ovolfsval  20796  ovolmge0  20802  ovollb2lem  20813  ovolunlem1a  20821  ovoliunlem1  20827  ovolicc1  20841  ovolicc2lem4  20845  ovolicc2lem5  20846  ioombl1lem2  20882  ioombl1lem4  20884  ovolfs2  20893  ioorcl  20899  uniiccdif  20900  uniioovol  20901  uniiccvol  20902  uniioombllem2a  20904  uniioombllem2  20905  uniioombllem3a  20906  uniioombllem3  20907  uniioombllem4  20908  uniioombllem5  20909  uniioombllem6  20910  dyadmbl  20922  volsup2  20927  volivth  20929  vitalilem1  20930  vitalilem2  20931  vitalilem4  20933  mbfimaopnlem  20975  cncombf  20978  cnmbf  20979  mbflimsup  20986  mbfi1fseqlem3  21037  mbfi1fseqlem4  21038  mbfi1fseqlem5  21039  itg2const2  21061  itg2lea  21064  itg2eqa  21065  itg2split  21069  itg2i1fseq  21075  itg2gt0  21080  limcco  21210  dvcl  21216  perfdvf  21220  dvreslem  21226  dvres2lem  21227  dvidlem  21232  dvcnp2  21236  dvmulbr  21255  dvferm1lem  21298  dvferm2lem  21300  dvferm  21302  rolle  21304  dvlipcn  21308  dvlip2  21309  c1liplem1  21310  c1lip2  21312  dvgt0lem1  21316  dvivthlem1  21322  dvivth  21324  lhop1lem  21327  lhop1  21328  lhop2  21329  lhop  21330  dvfsumlem1  21340  dvfsumlem2  21341  dvfsumlem3  21342  dvfsumlem4  21343  dvfsumrlimge0  21344  dvfsumrlim  21345  dvfsumrlim2  21346  dvfsum2  21348  ftc1lem5  21354  ftc1lem6  21355  itgsubstlem  21362  itgsubst  21363  mdegleb  21420  mdegaddle  21430  mdegvsca  21432  mdegmullem  21434  ig1peu  21528  plybss  21547  plyaddcl  21573  plymulcl  21574  plysubcl  21575  coeidlem  21590  coesub  21609  dgrmulc  21623  dgrcolem1  21625  dgrcolem2  21626  dgrco  21627  quotlem  21651  quotcl2  21653  quotdgr  21654  plyrem  21656  facth  21657  quotcan  21660  vieta1lem1  21661  vieta1  21663  elqaalem3  21672  aalioulem2  21684  aalioulem3  21685  taylfvallem1  21707  tayl0  21712  dvntaylp  21721  taylthlem1  21723  taylthlem2  21724  radcnvlt1  21768  radcnvle  21770  pserulm  21772  psercnlem2  21774  psercnlem1  21775  psercn  21776  pserdvlem1  21777  pserdvlem2  21778  abelthlem3  21783  abelthlem5  21785  abelthlem6  21786  abelth  21791  efcvx  21799  tanord  21879  tanregt0  21880  efif1olem4  21886  logtayl  21990  logccv  21993  cxpcn3  22071  ssscongptld  22105  chordthmlem  22112  chordthmlem4  22115  chordthmlem5  22116  chordthm  22117  heron  22118  asinrecl  22182  atantan  22203  dvatan  22215  leibpi  22222  rlimcnp  22244  efrlim  22248  cvxcl  22263  scvxcvx  22264  jensenlem1  22265  jensenlem2  22266  jensen  22267  amgmlem  22268  harmonicbnd3  22286  wilthlem1  22291  ftalem3  22297  ftalem5  22299  ftalem7  22301  basellem3  22305  basellem4  22306  basellem5  22307  ppisval  22326  chtf  22331  efchtcl  22334  chtge0  22335  sgmval2  22366  ppinprm  22375  chtprm  22376  chtnprm  22377  chtwordi  22379  chtdif  22381  efchtdvds  22382  sqff1o  22405  fsumdvdsdiaglem  22408  fsumdvdsdiag  22409  fsumdvdscom  22410  musum  22416  muinv  22418  dvdsmulf1o  22419  sgmmul  22425  chtlepsi  22430  chtleppi  22434  pclogsum  22439  chpval2  22442  chpchtsum  22443  chpub  22444  perfectlem2  22454  dchrelbasd  22463  dchrrcl  22464  dchrzrh1  22468  dchrzrhmul  22470  dchrinvcl  22477  dchrfi  22479  dchrghm  22480  dchr1  22481  dchrabs  22484  dchrinv  22485  dchrptlem2  22489  dchrsum2  22492  sumdchr2  22494  sum2dchr  22498  lgscl  22534  lgsquadlem1  22578  lgsquadlem2  22579  2sqlem6  22593  2sqlem8  22596  2sqlem9  22597  chebbnd1lem1  22603  chtppilimlem1  22607  rplogsumlem2  22619  dchrisum0flblem1  22642  rpvmasum2  22646  dchrisum0re  22647  dchrisum0lema  22648  dchrisum0lem1b  22649  dchrisum0lem1  22650  dchrisum0lem2a  22651  dchrisum0lem2  22652  dchrisum0lem3  22653  dchrisum0  22654  rplogsum  22661  dirith2  22662  mudivsum  22664  mulogsum  22666  mulog2sumlem2  22669  vmalogdivsum2  22672  logsqvma  22676  logsqvma2  22677  selberglem3  22681  selberg  22682  chpdifbndlem1  22687  selberg34r  22705  pntsval2  22710  pntrlog2bndlem1  22711  pntpbnd1a  22719  pntpbnd1  22720  pntpbnd2  22721  pntibndlem2a  22724  pntibndlem2  22725  pntibndlem3  22726  pntlemd  22728  padicabv  22764  axtgcgrrflx  22808  axtgcgrid  22809  axtgsegcon  22810  axtg5seg  22811  axtgbtwnid  22812  axtgpasch  22813  axtgcont1  22814  ttgcontlem1  22954  axlowdimlem16  23026  axcontlem10  23042  umgrass  23076  umgran0  23077  usgrass  23106  redwlk  23328  issubgo  23613  nvvop  23810  nmcnc  23914  ubthlem1  24094  minvecolem2  24099  minvecolem3  24100  minvecolem5  24105  minvecolem6  24106  minvecolem7  24107  hlimcaui  24462  pjocini  24924  fcnvgreu  25815  f1od2  25848  eliccelico  25890  elicoelioo  25891  iundisjfi  25903  iundisj2fi  25904  divnumden2  25910  xrsmulgzz  25962  ressmulgnn  25967  ressmulgnn0  25968  xrge0addass  25974  xrge0addgt0  25977  xrge0adddir  25979  xrge0adddi  25980  xrge0npcan  25981  fsumrp0cl  25982  archirngz  26030  archiabllem1b  26033  nn0srg  26063  rge0srg  26064  gsummpt2co  26101  regsumfsum  26103  xrge0tsmsd  26106  dvrdir  26111  rdivmuldivd  26112  dvrcan5  26114  elrhmunit  26141  rhmunitinv  26143  xrge0slmod  26166  cnre2csqima  26195  tpr2rico  26196  cnvordtrestixx  26197  ordtrestNEW  26205  xrge0iifcnv  26217  xrge0iifhom  26221  xrge0mulc1cn  26225  rge0scvg  26233  lmxrge0  26236  cnzh  26253  rezh  26254  qqhval2  26265  qqhvq  26270  qqhnm  26273  qqhcn  26274  qqhucn  26275  indsum  26333  indf1ofs  26336  esumel  26355  esumle  26362  esummono  26363  gsumesum  26364  esumlub  26365  esumlef  26367  esumcst  26368  esumfzf  26372  esumfsup  26373  esumfsupre  26374  esumpinfval  26376  esumpfinvallem  26377  esumpfinval  26378  esumpfinvalf  26379  esumpinfsum  26380  esumpcvgval  26381  esumpmono  26382  esummulc1  26384  esummulc2  26385  esumdivc  26386  hasheuni  26388  esumcvg  26389  sigainb  26433  measun  26479  measunl  26484  measiun  26486  meascnbl  26487  voliune  26499  volfiniune  26500  ddemeas  26506  dya2icoseg2  26547  dya2iocnrect  26550  sxbrsigalem2  26555  sibfof  26574  oddpwdc  26585  eulerpartlemgc  26593  eulerpartlemgvv  26607  eulerpartlemgf  26610  eulerpartlemgs2  26611  eulerpartlemn  26612  sseqf  26623  probun  26650  probdif  26651  probvalrnd  26655  probmeasb  26661  cndprobin  26665  bayesth  26670  ballotlemsdom  26742  ballotlemrv2  26752  ballotlemfrci  26758  sgnclre  26770  plymulx0  26796  signsply0  26800  signswch  26810  signstf  26815  signsvtn0  26819  signsvfn  26831  signlem0  26836  lgamgulmlem2  26864  lgamcvg2  26889  subfacp1lem5  26920  erdszelem4  26930  erdszelem6  26932  erdszelem7  26933  erdszelem8  26934  erdszelem9  26935  conpcon  26972  cvxscon  26980  rescon  26983  iccllyscon  26987  rellyscon  26988  cvmsrcl  27001  cvmliftmolem2  27019  cvmlift2lem12  27051  cvmlift3  27065  snmlval  27068  clim2prod  27250  ntrivcvg  27259  ntrivcvgfvn0  27261  ntrivcvgtail  27262  ntrivcvgmullem  27263  ntrivcvgmul  27264  prodrblem  27289  prodmolem2a  27294  mblfinlem2  28273  itg2addnclem3  28289  itg2addnc  28290  itg2gt0cn  28291  ftc1cnnclem  28309  ftc1anclem6  28316  islocfin  28412  neibastop1  28424  fdc  28485  prdsbnd  28536  ismtyval  28543  heiborlem3  28556  heiborlem5  28558  heiborlem10  28563  rrnequiv  28578  eldiophb  28940  4rexfrabdioph  28981  6rexfrabdioph  28982  diophren  28997  rencldnfilem  29004  pellexlem3  29017  pellfundglb  29071  rmxypairf1o  29097  rmxycomplete  29103  rmxyneg  29106  rmxyadd  29107  rmxy1  29108  rmxy0  29109  monotuz  29127  jm2.22  29189  aomclem2  29253  isnumbasgrp  29308  dfacbasgrp  29309  hbtlem2  29325  hbt  29331  elmnc  29338  issdrg  29399  cntzsdrg  29404  mon1psubm  29419  areaquad  29437  stoweidlem26  29667  stoweidlem51  29692  ige2m1fz  30052  suctrALT  31264  suctrALT3  31362  chordthmALT  31371  iunconlem2  31373  bnj1213  31494  bnj1417  31734  osumcllem7N  33179  pexmidlem4N  33190