Theorem feq1d 6683

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6533  df-fn 6534  df-f 6535

This theorem is used by:  feq1dd  6684  feq12d  6689  fco2  6728  fssres2  6742  fresin  6743  fresaun  6745  fmpt3d  7108  fressnfv  7156  f2ndf  8120  eroprf  8820  curf  8874  uncf  8875  pmresg  8882  pw2f1olem  9084  ordtypelem4  9499  canthp1lem2  10719  fseq1p1m1  13712  repsf  14904  rlimres  15705  lo1res  15706  vdwapf  17130  fsets  17327  mrcf  17763  cofucl  18043  funcres  18051  funcestrcsetclem9  18302  1stfcl  18351  2ndfcl  18352  evlfcl  18376  yonedalem4c  18431  pmtrfinv  19655  pmtrff1o  19657  pmtrfcnv  19658  efgtf  19916  gsumzres  20103  isphld  21940  pjf  21999  frlmup1  22084  psrass1lem  22221  coe1f2  22507  lmbr  23556  tsmsres  24443  prdsdsf  24666  imasdsf1olem  24672  blfps  24705  blf  24706  tngngp2  24951  rrxmet  25709  ovolctb  25791  itg2monolem1  26051  itg2monolem2  26052  itg2monolem3  26053  itg2mono  26054  dvres  26211  dvres3a  26214  dvnff  26223  dvcmulf  26245  dvmptcl  26259  dvmptco  26272  dvlipcn  26294  dvgt0lem1  26302  itgsubstlem  26348  itgpowd  26350  dgrlem  26528  taylthlem1  26682  ulmval  26689  lgsfcl3  27627  midf  29263  pfxwlk  30248  grpodivf  31122  nvmf  31229  imsdf  31273  ipf  31297  0oo  31373  hoaddcl  32342  homulcl  32343  hosubcl  32357  fmptcof2  33233  ofoprabco  33240  fpwrelmap  33307  indf1ofs  33415  fedgmullem1  34243  sitmf  34967  fibp1  35016  ccatmulgnn0dir  35157  reprsuc  35227  cvmliftlem6  36024  cvmliftlem10  36028  mrsubff  36246  msubff  36264  tailf  37133  poimirlem24  38530  ftc1anclem3  38581  rrnmet  38731  tendoplcl  41806  tendoicl  41821  intlewftc  43079  aks6d1c2  43148  aks6d1c6lem3  43190  pw2f1ocnv  43997  seff  45252  expgrowth  45278  dvnmul  46897  dvnprodlem2  46901  dvnprodlem3  46902  voliooicof  46950  stoweidlem34  46988  stoweidlem42  46996  stoweidlem48  47002  dirkerf  47051  fourierdlem41  47102  fourierdlem51  47111  fourierdlem57  47117  fourierdlem60  47120  fourierdlem61  47121  fourierdlem73  47133  fourierdlem75  47135  fourierdlem103  47163  fourierdlem104  47164  etransclem1  47189  etransclem2  47190  etransclem20  47208  etransclem33  47221  etransclem46  47234  sge0isum  47381  sge0seq  47400  isomenndlem  47484  ovnf  47517  ovnsubaddlem1  47524  hsphoif  47530  hoidmvlelem2  47550  hoidmvlelem3  47551  ovnhoilem1  47555  ovnhoilem2  47556  ovncvr2  47565  hoidifhspf  47572  hspmbllem2  47581  iccvonmbllem  47632  vonioolem1  47634  vonioolem2  47635  vonicclem1  47637  vonicclem2  47638  smfsupdmmbllem  47798  smfinfdmmbllem  47802  fsetsniunop  48063  1hegrlfgr  49174  funcringcsetcALTV2lem3  49333  funcringcsetcALTV2lem9  49339  funcringcsetclem3ALTV  49356  funcringcsetclem9ALTV  49362  fdivmptf  49597  refdivmptf  49598  itcovalendof  49725  ackendofnn0  49740  fucoppcid  50460  functermc  50560