Theorem feq1d 6633

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ⟶wf 6477

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-fun 6483  df-fn 6484  df-f 6485

This theorem is referenced by:  feq1dd  6634  feq12d  6639  fco2  6677  fssres2  6691  fresin  6692  fresaun  6694  fmpt3d  7049  fressnfv  7093  f2ndf  8050  eroprf  8739  pmresg  8794  pw2f1olem  8994  ordtypelem4  9407  canthp1lem2  10541  fseq1p1m1  13495  repsf  14677  rlimres  15462  lo1res  15463  vdwapf  16881  fsets  17077  mrcf  17512  cofucl  17792  funcres  17800  funcestrcsetclem9  18051  1stfcl  18100  2ndfcl  18101  evlfcl  18125  yonedalem4c  18180  pmtrfinv  19371  pmtrff1o  19373  pmtrfcnv  19374  efgtf  19632  gsumzres  19819  isphld  21589  pjf  21648  frlmup1  21733  psrass1lem  21867  coe1f2  22120  lmbr  23171  tsmsres  24057  prdsdsf  24280  imasdsf1olem  24286  blfps  24319  blf  24320  tngngp2  24565  rrxmet  25333  ovolctb  25416  itg2monolem1  25676  itg2monolem2  25677  itg2monolem3  25678  itg2mono  25679  dvres  25837  dvres3a  25840  dvnff  25850  dvcmulf  25873  dvmptcl  25888  dvmptco  25901  dvlipcn  25924  dvgt0lem1  25932  itgsubstlem  25980  itgpowd  25982  dgrlem  26159  taylthlem1  26306  ulmval  26314  lgsfcl3  27254  midf  28752  grpodivf  30513  nvmf  30620  imsdf  30664  ipf  30688  0oo  30764  hoaddcl  31733  homulcl  31734  hosubcl  31748  fmptcof2  32634  ofoprabco  32641  fpwrelmap  32711  indf1ofs  32842  fedgmullem1  33637  sitmf  34360  fibp1  34409  ccatmulgnn0dir  34550  reprsuc  34623  pfxwlk  35156  cvmliftlem6  35322  cvmliftlem10  35326  mrsubff  35544  msubff  35562  tailf  36408  curf  37637  uncf  37638  poimirlem24  37683  ftc1anclem3  37734  rrnmet  37868  tendoplcl  40819  tendoicl  40834  intlewftc  42093  aks6d1c2  42162  aks6d1c6lem3  42204  pw2f1ocnv  43069  seff  44341  expgrowth  44367  dvnmul  45980  dvnprodlem2  45984  dvnprodlem3  45985  voliooicof  46033  stoweidlem34  46071  stoweidlem42  46079  stoweidlem48  46085  dirkerf  46134  fourierdlem41  46185  fourierdlem51  46194  fourierdlem57  46200  fourierdlem60  46203  fourierdlem61  46204  fourierdlem73  46216  fourierdlem75  46218  fourierdlem103  46246  fourierdlem104  46247  etransclem1  46272  etransclem2  46273  etransclem20  46291  etransclem33  46304  etransclem46  46317  sge0isum  46464  sge0seq  46483  isomenndlem  46567  hoicvr  46585  ovnf  46600  ovnsubaddlem1  46607  hsphoif  46613  hoidmvlelem2  46633  hoidmvlelem3  46634  ovnhoilem1  46638  ovnhoilem2  46639  ovncvr2  46648  hoidifhspf  46655  hspmbllem2  46664  iccvonmbllem  46715  vonioolem1  46717  vonioolem2  46718  vonicclem1  46720  vonicclem2  46721  smfsupdmmbllem  46881  smfinfdmmbllem  46885  fsetsniunop  47079  1hegrlfgr  48162  funcringcsetcALTV2lem3  48322  funcringcsetcALTV2lem9  48328  funcringcsetclem3ALTV  48345  funcringcsetclem9ALTV  48351  fdivmptf  48572  refdivmptf  48573  itcovalendof  48700  ackendofnn0  48715  fucoppcid  49439  functermc  49539