Theorem feq1d 6699

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ⟶wf 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-fun 6542  df-fn 6543  df-f 6544

This theorem is referenced by:  feq12d  6702  fco2  6741  fssres2  6756  fresin  6757  fresaun  6759  fmpt3d  7112  fressnfv  7154  f2ndf  8102  eroprf  8805  pmresg  8860  pw2f1olem  9072  ordtypelem4  9512  canthp1lem2  10644  fseq1p1m1  13571  repsf  14719  rlimres  15498  lo1res  15499  vdwapf  16901  fsets  17098  mrcf  17549  cofucl  17834  funcres  17842  funcestrcsetclem9  18096  1stfcl  18145  2ndfcl  18146  evlfcl  18171  yonedalem4c  18226  pmtrfinv  19323  pmtrff1o  19325  pmtrfcnv  19326  efgtf  19584  gsumzres  19771  isphld  21198  pjf  21259  frlmup1  21344  psrass1lemOLD  21484  psrass1lem  21487  coe1f2  21724  lmbr  22753  tsmsres  23639  prdsdsf  23864  imasdsf1olem  23870  blfps  23903  blf  23904  tngngp2  24160  rrxmet  24916  ovolctb  24998  itg2monolem1  25259  itg2monolem2  25260  itg2monolem3  25261  itg2mono  25262  dvres  25419  dvres3a  25422  dvnff  25431  dvcmulf  25453  dvmptcl  25467  dvmptco  25480  dvlipcn  25502  dvgt0lem1  25510  itgsubstlem  25556  itgpowd  25558  dgrlem  25734  taylthlem1  25876  ulmval  25883  lgsfcl3  26810  midf  28016  grpodivf  29778  nvmf  29885  imsdf  29929  ipf  29953  0oo  30029  hoaddcl  30998  homulcl  30999  hosubcl  31013  fmptcof2  31869  ofoprabco  31876  fpwrelmap  31945  fedgmullem1  32702  indf1ofs  33012  sitmf  33339  fibp1  33388  ccatmulgnn0dir  33541  reprsuc  33615  pfxwlk  34102  cvmliftlem6  34269  cvmliftlem10  34273  mrsubff  34491  msubff  34509  tailf  35248  curf  36454  uncf  36455  poimirlem24  36500  ftc1anclem3  36551  rrnmet  36685  tendoplcl  39640  tendoicl  39655  intlewftc  40914  pw2f1ocnv  41761  seff  43053  expgrowth  43079  feq1dd  43848  dvnmul  44645  dvnprodlem2  44649  dvnprodlem3  44650  voliooicof  44698  stoweidlem34  44736  stoweidlem42  44744  stoweidlem48  44750  dirkerf  44799  fourierdlem41  44850  fourierdlem51  44859  fourierdlem57  44865  fourierdlem60  44868  fourierdlem61  44869  fourierdlem73  44881  fourierdlem75  44883  fourierdlem103  44911  fourierdlem104  44912  etransclem1  44937  etransclem2  44938  etransclem20  44956  etransclem33  44969  etransclem46  44982  sge0isum  45129  sge0seq  45148  isomenndlem  45232  hoicvr  45250  ovnf  45265  ovnsubaddlem1  45272  hsphoif  45278  hoidmvlelem2  45298  hoidmvlelem3  45299  ovnhoilem1  45303  ovnhoilem2  45304  ovncvr2  45313  hoidifhspf  45320  hspmbllem2  45329  iccvonmbllem  45380  vonioolem1  45382  vonioolem2  45383  vonicclem1  45385  vonicclem2  45386  smfsupdmmbllem  45546  smfinfdmmbllem  45550  fsetsniunop  45745  1hegrlfgr  46496  funcringcsetcALTV2lem3  46889  funcringcsetcALTV2lem9  46895  funcringcsetclem3ALTV  46912  funcringcsetclem9ALTV  46918  fdivmptf  47180  refdivmptf  47181  itcovalendof  47308  ackendofnn0  47323