Theorem feq1d 6636

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  ⟶wf 6475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-br 5093  df-opab 5155  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-fun 6481  df-fn 6482  df-f 6483

This theorem is referenced by:  feq12d  6639  fco2  6678  fssres2  6693  fresin  6694  fresaun  6696  fmpt3d  7046  fressnfv  7088  f2ndf  8028  eroprf  8675  pmresg  8729  pw2f1olem  8941  ordtypelem4  9378  canthp1lem2  10510  fseq1p1m1  13431  repsf  14584  rlimres  15366  lo1res  15367  vdwapf  16770  fsets  16967  mrcf  17415  cofucl  17700  funcres  17708  funcestrcsetclem9  17962  1stfcl  18011  2ndfcl  18012  evlfcl  18037  yonedalem4c  18092  pmtrfinv  19165  pmtrff1o  19167  pmtrfcnv  19168  efgtf  19423  gsumzres  19605  isphld  20965  pjf  21026  frlmup1  21111  psrass1lemOLD  21249  psrass1lem  21252  coe1f2  21486  lmbr  22515  tsmsres  23401  prdsdsf  23626  imasdsf1olem  23632  blfps  23665  blf  23666  tngngp2  23922  rrxmet  24678  ovolctb  24760  itg2monolem1  25021  itg2monolem2  25022  itg2monolem3  25023  itg2mono  25024  dvres  25181  dvres3a  25184  dvnff  25193  dvcmulf  25215  dvmptcl  25229  dvmptco  25242  dvlipcn  25264  dvgt0lem1  25272  itgsubstlem  25318  itgpowd  25320  dgrlem  25496  taylthlem1  25638  ulmval  25645  lgsfcl3  26572  midf  27426  grpodivf  29188  nvmf  29295  imsdf  29339  ipf  29363  0oo  29439  hoaddcl  30408  homulcl  30409  hosubcl  30423  fmptcof2  31281  ofoprabco  31288  fpwrelmap  31355  fedgmullem1  32008  indf1ofs  32292  sitmf  32619  fibp1  32668  ccatmulgnn0dir  32821  reprsuc  32895  pfxwlk  33384  cvmliftlem6  33551  cvmliftlem10  33555  mrsubff  33773  msubff  33791  tailf  34660  curf  35868  uncf  35869  poimirlem24  35914  ftc1anclem3  35965  rrnmet  36100  tendoplcl  39057  tendoicl  39072  intlewftc  40331  pw2f1ocnv  41130  seff  42257  expgrowth  42283  feq1dd  43039  dvnmul  43829  dvnprodlem2  43833  dvnprodlem3  43834  voliooicof  43882  stoweidlem34  43920  stoweidlem42  43928  stoweidlem48  43934  dirkerf  43983  fourierdlem41  44034  fourierdlem51  44043  fourierdlem57  44049  fourierdlem60  44052  fourierdlem61  44053  fourierdlem73  44065  fourierdlem75  44067  fourierdlem103  44095  fourierdlem104  44096  etransclem1  44121  etransclem2  44122  etransclem20  44140  etransclem33  44153  etransclem46  44166  sge0isum  44311  sge0seq  44330  isomenndlem  44414  hoicvr  44432  ovnf  44447  ovnsubaddlem1  44454  hsphoif  44460  hoidmvlelem2  44480  hoidmvlelem3  44481  ovnhoilem1  44485  ovnhoilem2  44486  ovncvr2  44495  hoidifhspf  44502  hspmbllem2  44511  iccvonmbllem  44562  vonioolem1  44564  vonioolem2  44565  vonicclem1  44567  vonicclem2  44568  fsetsniunop  44903  1hegrlfgr  45654  funcringcsetcALTV2lem3  45956  funcringcsetcALTV2lem9  45962  funcringcsetclem3ALTV  45979  funcringcsetclem9ALTV  45985  fdivmptf  46247  refdivmptf  46248  itcovalendof  46375  ackendofnn0  46390