Theorem feq1d 6569

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  feq12d  6572  fco2  6611  fssres2  6626  fresin  6627  fresaun  6629  fmpt3d  6972  fressnfv  7014  f2ndf  7932  eroprf  8562  pmresg  8616  pw2f1olem  8816  ordtypelem4  9210  canthp1lem2  10340  fseq1p1m1  13259  repsf  14414  rlimres  15195  lo1res  15196  vdwapf  16601  fsets  16798  mrcf  17235  cofucl  17519  funcres  17527  funcestrcsetclem9  17781  1stfcl  17830  2ndfcl  17831  evlfcl  17856  yonedalem4c  17911  pmtrfinv  18984  pmtrff1o  18986  pmtrfcnv  18987  efgtf  19243  gsumzres  19425  isphld  20771  pjf  20830  frlmup1  20915  psrass1lemOLD  21053  psrass1lem  21056  coe1f2  21290  lmbr  22317  tsmsres  23203  prdsdsf  23428  imasdsf1olem  23434  blfps  23467  blf  23468  tngngp2  23722  rrxmet  24477  ovolctb  24559  itg2monolem1  24820  itg2monolem2  24821  itg2monolem3  24822  itg2mono  24823  dvres  24980  dvres3a  24983  dvnff  24992  dvcmulf  25014  dvmptcl  25028  dvmptco  25041  dvlipcn  25063  dvgt0lem1  25071  itgsubstlem  25117  itgpowd  25119  dgrlem  25295  taylthlem1  25437  ulmval  25444  lgsfcl3  26371  midf  27041  grpodivf  28801  nvmf  28908  imsdf  28952  ipf  28976  0oo  29052  hoaddcl  30021  homulcl  30022  hosubcl  30036  fmptcof2  30896  ofoprabco  30903  fpwrelmap  30970  fedgmullem1  31612  indf1ofs  31894  sitmf  32219  fibp1  32268  ccatmulgnn0dir  32421  reprsuc  32495  pfxwlk  32985  cvmliftlem6  33152  cvmliftlem10  33156  mrsubff  33374  msubff  33392  tailf  34491  curf  35682  uncf  35683  poimirlem24  35728  ftc1anclem3  35779  rrnmet  35914  tendoplcl  38722  tendoicl  38737  intlewftc  39997  pw2f1ocnv  40775  seff  41816  expgrowth  41842  feq1dd  42592  dvnmul  43374  dvnprodlem2  43378  dvnprodlem3  43379  voliooicof  43427  stoweidlem34  43465  stoweidlem42  43473  stoweidlem48  43479  dirkerf  43528  fourierdlem41  43579  fourierdlem51  43588  fourierdlem57  43594  fourierdlem60  43597  fourierdlem61  43598  fourierdlem73  43610  fourierdlem75  43612  fourierdlem103  43640  fourierdlem104  43641  etransclem1  43666  etransclem2  43667  etransclem20  43685  etransclem33  43698  etransclem46  43711  sge0isum  43855  sge0seq  43874  isomenndlem  43958  hoicvr  43976  ovnf  43991  ovnsubaddlem1  43998  hsphoif  44004  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoilem1  44029  ovnhoilem2  44030  ovncvr2  44039  hoidifhspf  44046  hspmbllem2  44055  iccvonmbllem  44106  vonioolem1  44108  vonioolem2  44109  vonicclem1  44111  vonicclem2  44112  fsetsniunop  44430  1hegrlfgr  45182  funcringcsetcALTV2lem3  45484  funcringcsetcALTV2lem9  45490  funcringcsetclem3ALTV  45507  funcringcsetclem9ALTV  45513  fdivmptf  45775  refdivmptf  45776  itcovalendof  45903  ackendofnn0  45918