Theorem feq1d 5722

Description: Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)

Hypothesis

Ref	Expression
feq1d.1

Assertion

Ref	Expression
feq1d

Proof of Theorem feq1d

Step	Hyp	Ref	Expression
1		feq1d.1	. 2
2		feq1 5718	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  -->wf 5589

This theorem is referenced by:  feq12d  5725  fco2  5747  fssres2  5758  fresin  5759  fresaun  5761  fmptco  6064  fressnfv  6085  off  6554  caofinvl  6567  curry1f  6894  curry2f  6896  f2ndf  6906  eroprf  7428  pmresg  7466  pw2f1olem  7641  ordtypelem4  7967  fseqenlem1  8426  canthp1lem2  9052  fseq1p1m1  11781  repsf  12745  rlimres  13381  lo1res  13382  rpnnen2lem2  13949  1arithlem3  14443  vdwapf  14490  fsets  14658  mrcf  15006  cofucl  15257  funcres  15265  homaf  15357  1stfcl  15466  2ndfcl  15467  prfcl  15472  evlfcl  15491  curf1cl  15497  yonedalem4c  15546  vrmdf  16026  pmtrf  16480  pmtrfinv  16486  pmtrff1o  16488  pmtrfcnv  16489  psgnunilem5  16519  pj1f  16715  efgtf  16740  vrgpf  16786  gsumzres  16914  gsumzresOLD  16918  gsummptfsadd  16940  gsummptfsaddOLD  16941  gsummptfssub  16976  lspf  17620  psrass1lem  18029  subrgpsr  18074  mvrf  18080  coe1f2  18248  isphld  18689  pjf  18744  uvcff  18822  frlmup1  18832  cpm2mf  19253  lmbr  19759  tsmsresOLD  20645  tsmsres  20646  prdsdsf  20870  imasdsf1olem  20876  blfps  20909  blf  20910  nmf2  21113  tngngp2  21166  nmof  21226  cphnmf  21642  rrxmet  21835  ovolctb  21901  uniioombllem2  21992  mbfi1fseqlem3  22124  itg2monolem1  22157  itg2monolem2  22158  itg2monolem3  22159  itg2mono  22160  itg2cnlem1  22168  dvres  22315  dvres3a  22318  dvnff  22326  dvcmulf  22348  dvmptcl  22362  dvmptco  22375  dvlipcn  22395  dvgt0lem1  22403  dvle  22408  itgsubstlem  22449  dgrlem  22626  taylpf  22761  taylthlem1  22768  ulmval  22775  ulmshftlem  22784  ulmshft  22785  ulmdvlem1  22795  psergf  22807  pserdvlem2  22823  lgsfcl3  23592  midf  24142  lmif  24151  vdgrf  24898  vdgrfif  24899  grpodivf  25248  nvmf  25541  imsdf  25595  ipf  25626  0oo  25704  hoaddcl  26677  homulcl  26678  hosubcl  26692  brafn  26866  kbop  26872  off2  27481  fmpt3d  27496  fmptcof2  27502  ofoprabco  27505  fpwrelmap  27556  indf1ofs  28039  fibp1  28340  ccatmulgnn0dir  28496  cvmliftlem6  28735  cvmliftlem10  28739  mrsubff  28872  msubff  28890  ftc1anclem3  30092  tailf  30193  rrnmet  30325  pw2f1ocnv  30979  itgpowd  31182  seff  31189  expgrowth  31240  feq1dd  31442  dvnmul  31740  dvnprodlem2  31744  dvnprodlem3  31745  stoweidlem34  31816  stoweidlem42  31824  stoweidlem48  31830  dirkerf  31879  fourierdlem41  31930  fourierdlem51  31940  fourierdlem57  31946  fourierdlem60  31949  fourierdlem61  31950  fourierdlem73  31962  fourierdlem75  31964  fourierdlem103  31992  fourierdlem104  31993  etransclem1  32018  etransclem2  32019  etransclem20  32037  etransclem33  32050  etransclem46  32063  funcestrcsetclem3  32648  funcestrcsetclem9  32654  funcsetcestrclem3  32662  funcringcsetcOLD2lem3  32846  funcringcsetcOLD2lem9  32852  funcringcsetclem3OLD  32869  funcringcsetclem9OLD  32875  tendoplcl  36507  tendoicl  36522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-fun 5595  df-fn 5596  df-f 5597