Theorem feq1d 6677

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-fun 6527  df-fn 6528  df-f 6529

This theorem is referenced by:  feq1dd  6678  feq12d  6683  fco2  6722  fssres2  6736  fresin  6737  fresaun  6739  fmpt3d  7101  fressnfv  7147  f2ndf  8103  eroprf  8801  pmresg  8856  pw2f1olem  9057  ordtypelem4  9471  canthp1lem2  10626  fseq1p1m1  13617  repsf  14800  rlimres  15599  lo1res  15600  vdwapf  17022  fsets  17219  mrcf  17655  cofucl  17935  funcres  17943  funcestrcsetclem9  18194  1stfcl  18243  2ndfcl  18244  evlfcl  18268  yonedalem4c  18323  pmtrfinv  19522  pmtrff1o  19524  pmtrfcnv  19525  efgtf  19783  gsumzres  19970  isphld  21764  pjf  21823  frlmup1  21908  psrass1lem  22043  coe1f2  22329  lmbr  23376  tsmsres  24262  prdsdsf  24485  imasdsf1olem  24491  blfps  24524  blf  24525  tngngp2  24770  rrxmet  25528  ovolctb  25610  itg2monolem1  25870  itg2monolem2  25871  itg2monolem3  25872  itg2mono  25873  dvres  26031  dvres3a  26034  dvnff  26043  dvcmulf  26065  dvmptcl  26079  dvmptco  26092  dvlipcn  26114  dvgt0lem1  26122  itgsubstlem  26168  itgpowd  26170  dgrlem  26347  taylthlem1  26494  ulmval  26501  lgsfcl3  27440  midf  29028  grpodivf  30799  nvmf  30906  imsdf  30950  ipf  30974  0oo  31050  hoaddcl  32019  homulcl  32020  hosubcl  32034  fmptcof2  32914  ofoprabco  32921  fpwrelmap  32990  indf1ofs  33099  fedgmullem1  33936  sitmf  34659  fibp1  34708  ccatmulgnn0dir  34849  reprsuc  34919  pfxwlk  35487  cvmliftlem6  35653  cvmliftlem10  35657  mrsubff  35875  msubff  35893  tailf  36748  curf  38109  uncf  38110  poimirlem24  38155  ftc1anclem3  38206  rrnmet  38340  tendoplcl  41417  tendoicl  41432  intlewftc  42690  aks6d1c2  42759  aks6d1c6lem3  42801  pw2f1ocnv  43626  seff  44883  expgrowth  44909  dvnmul  46515  dvnprodlem2  46519  dvnprodlem3  46520  voliooicof  46568  stoweidlem34  46606  stoweidlem42  46614  stoweidlem48  46620  dirkerf  46669  fourierdlem41  46720  fourierdlem51  46729  fourierdlem57  46735  fourierdlem60  46738  fourierdlem61  46739  fourierdlem73  46751  fourierdlem75  46753  fourierdlem103  46781  fourierdlem104  46782  etransclem1  46807  etransclem2  46808  etransclem20  46826  etransclem33  46839  etransclem46  46852  sge0isum  46999  sge0seq  47018  isomenndlem  47102  ovnf  47135  ovnsubaddlem1  47142  hsphoif  47148  hoidmvlelem2  47168  hoidmvlelem3  47169  ovnhoilem1  47173  ovnhoilem2  47174  ovncvr2  47183  hoidifhspf  47190  hspmbllem2  47199  iccvonmbllem  47250  vonioolem1  47252  vonioolem2  47253  vonicclem1  47255  vonicclem2  47256  smfsupdmmbllem  47416  smfinfdmmbllem  47420  fsetsniunop  47641  1hegrlfgr  48752  funcringcsetcALTV2lem3  48912  funcringcsetcALTV2lem9  48918  funcringcsetclem3ALTV  48935  funcringcsetclem9ALTV  48941  fdivmptf  49172  refdivmptf  49173  itcovalendof  49300  ackendofnn0  49315  fucoppcid  50037  functermc  50137