Theorem feq1d 6703

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 6699	. 2 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-fun 6546  df-fn 6547  df-f 6548

This theorem is referenced by:  feq12d  6706  fco2  6745  fssres2  6760  fresin  6761  fresaun  6763  fmpt3d  7116  fressnfv  7158  f2ndf  8106  eroprf  8809  pmresg  8864  pw2f1olem  9076  ordtypelem4  9516  canthp1lem2  10648  fseq1p1m1  13575  repsf  14723  rlimres  15502  lo1res  15503  vdwapf  16905  fsets  17102  mrcf  17553  cofucl  17838  funcres  17846  funcestrcsetclem9  18100  1stfcl  18149  2ndfcl  18150  evlfcl  18175  yonedalem4c  18230  pmtrfinv  19329  pmtrff1o  19331  pmtrfcnv  19332  efgtf  19590  gsumzres  19777  isphld  21207  pjf  21268  frlmup1  21353  psrass1lemOLD  21493  psrass1lem  21496  coe1f2  21733  lmbr  22762  tsmsres  23648  prdsdsf  23873  imasdsf1olem  23879  blfps  23912  blf  23913  tngngp2  24169  rrxmet  24925  ovolctb  25007  itg2monolem1  25268  itg2monolem2  25269  itg2monolem3  25270  itg2mono  25271  dvres  25428  dvres3a  25431  dvnff  25440  dvcmulf  25462  dvmptcl  25476  dvmptco  25489  dvlipcn  25511  dvgt0lem1  25519  itgsubstlem  25565  itgpowd  25567  dgrlem  25743  taylthlem1  25885  ulmval  25892  lgsfcl3  26821  midf  28027  grpodivf  29791  nvmf  29898  imsdf  29942  ipf  29966  0oo  30042  hoaddcl  31011  homulcl  31012  hosubcl  31026  fmptcof2  31882  ofoprabco  31889  fpwrelmap  31958  fedgmullem1  32714  indf1ofs  33024  sitmf  33351  fibp1  33400  ccatmulgnn0dir  33553  reprsuc  33627  pfxwlk  34114  cvmliftlem6  34281  cvmliftlem10  34285  mrsubff  34503  msubff  34521  tailf  35260  curf  36466  uncf  36467  poimirlem24  36512  ftc1anclem3  36563  rrnmet  36697  tendoplcl  39652  tendoicl  39667  intlewftc  40926  pw2f1ocnv  41776  seff  43068  expgrowth  43094  feq1dd  43863  dvnmul  44659  dvnprodlem2  44663  dvnprodlem3  44664  voliooicof  44712  stoweidlem34  44750  stoweidlem42  44758  stoweidlem48  44764  dirkerf  44813  fourierdlem41  44864  fourierdlem51  44873  fourierdlem57  44879  fourierdlem60  44882  fourierdlem61  44883  fourierdlem73  44895  fourierdlem75  44897  fourierdlem103  44925  fourierdlem104  44926  etransclem1  44951  etransclem2  44952  etransclem20  44970  etransclem33  44983  etransclem46  44996  sge0isum  45143  sge0seq  45162  isomenndlem  45246  hoicvr  45264  ovnf  45279  ovnsubaddlem1  45286  hsphoif  45292  hoidmvlelem2  45312  hoidmvlelem3  45313  ovnhoilem1  45317  ovnhoilem2  45318  ovncvr2  45327  hoidifhspf  45334  hspmbllem2  45343  iccvonmbllem  45394  vonioolem1  45396  vonioolem2  45397  vonicclem1  45399  vonicclem2  45400  smfsupdmmbllem  45560  smfinfdmmbllem  45564  fsetsniunop  45759  1hegrlfgr  46510  funcringcsetcALTV2lem3  46936  funcringcsetcALTV2lem9  46942  funcringcsetclem3ALTV  46959  funcringcsetclem9ALTV  46965  fdivmptf  47227  refdivmptf  47228  itcovalendof  47355  ackendofnn0  47370