Theorem feq1d 6644

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

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  feq1dd  6645  feq12d  6650  fco2  6688  fssres2  6702  fresin  6703  fresaun  6705  fmpt3d  7061  fressnfv  7105  f2ndf  8062  eroprf  8752  pmresg  8808  pw2f1olem  9009  ordtypelem4  9426  canthp1lem2  10564  fseq1p1m1  13514  repsf  14696  rlimres  15481  lo1res  15482  vdwapf  16900  fsets  17096  mrcf  17532  cofucl  17812  funcres  17820  funcestrcsetclem9  18071  1stfcl  18120  2ndfcl  18121  evlfcl  18145  yonedalem4c  18200  pmtrfinv  19390  pmtrff1o  19392  pmtrfcnv  19393  efgtf  19651  gsumzres  19838  isphld  21609  pjf  21668  frlmup1  21753  psrass1lem  21888  coe1f2  22150  lmbr  23202  tsmsres  24088  prdsdsf  24311  imasdsf1olem  24317  blfps  24350  blf  24351  tngngp2  24596  rrxmet  25364  ovolctb  25447  itg2monolem1  25707  itg2monolem2  25708  itg2monolem3  25709  itg2mono  25710  dvres  25868  dvres3a  25871  dvnff  25881  dvcmulf  25904  dvmptcl  25919  dvmptco  25932  dvlipcn  25955  dvgt0lem1  25963  itgsubstlem  26011  itgpowd  26013  dgrlem  26190  taylthlem1  26337  ulmval  26345  lgsfcl3  27285  midf  28848  grpodivf  30613  nvmf  30720  imsdf  30764  ipf  30788  0oo  30864  hoaddcl  31833  homulcl  31834  hosubcl  31848  fmptcof2  32735  ofoprabco  32742  fpwrelmap  32812  indf1ofs  32948  fedgmullem1  33786  sitmf  34509  fibp1  34558  ccatmulgnn0dir  34699  reprsuc  34772  pfxwlk  35318  cvmliftlem6  35484  cvmliftlem10  35488  mrsubff  35706  msubff  35724  tailf  36569  curf  37795  uncf  37796  poimirlem24  37841  ftc1anclem3  37892  rrnmet  38026  tendoplcl  41037  tendoicl  41052  intlewftc  42311  aks6d1c2  42380  aks6d1c6lem3  42422  pw2f1ocnv  43275  seff  44546  expgrowth  44572  dvnmul  46183  dvnprodlem2  46187  dvnprodlem3  46188  voliooicof  46236  stoweidlem34  46274  stoweidlem42  46282  stoweidlem48  46288  dirkerf  46337  fourierdlem41  46388  fourierdlem51  46397  fourierdlem57  46403  fourierdlem60  46406  fourierdlem61  46407  fourierdlem73  46419  fourierdlem75  46421  fourierdlem103  46449  fourierdlem104  46450  etransclem1  46475  etransclem2  46476  etransclem20  46494  etransclem33  46507  etransclem46  46520  sge0isum  46667  sge0seq  46686  isomenndlem  46770  hoicvr  46788  ovnf  46803  ovnsubaddlem1  46810  hsphoif  46816  hoidmvlelem2  46836  hoidmvlelem3  46837  ovnhoilem1  46841  ovnhoilem2  46842  ovncvr2  46851  hoidifhspf  46858  hspmbllem2  46867  iccvonmbllem  46918  vonioolem1  46920  vonioolem2  46921  vonicclem1  46923  vonicclem2  46924  smfsupdmmbllem  47084  smfinfdmmbllem  47088  fsetsniunop  47291  1hegrlfgr  48374  funcringcsetcALTV2lem3  48534  funcringcsetcALTV2lem9  48540  funcringcsetclem3ALTV  48557  funcringcsetclem9ALTV  48563  fdivmptf  48783  refdivmptf  48784  itcovalendof  48911  ackendofnn0  48926  fucoppcid  49649  functermc  49749