Theorem feq1d 6669

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  ⟶wf 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-fun 6519  df-fn 6520  df-f 6521

This theorem is referenced by:  feq1dd  6670  feq12d  6675  fco2  6714  fssres2  6728  fresin  6729  fresaun  6731  fmpt3d  7093  fressnfv  7139  f2ndf  8094  eroprf  8792  pmresg  8848  pw2f1olem  9049  ordtypelem4  9466  canthp1lem2  10608  fseq1p1m1  13600  repsf  14783  rlimres  15568  lo1res  15569  vdwapf  16991  fsets  17188  mrcf  17624  cofucl  17904  funcres  17912  funcestrcsetclem9  18163  1stfcl  18212  2ndfcl  18213  evlfcl  18237  yonedalem4c  18292  pmtrfinv  19484  pmtrff1o  19486  pmtrfcnv  19487  efgtf  19745  gsumzres  19932  isphld  21686  pjf  21745  frlmup1  21830  psrass1lem  21965  coe1f2  22251  lmbr  23298  tsmsres  24184  prdsdsf  24407  imasdsf1olem  24413  blfps  24446  blf  24447  tngngp2  24692  rrxmet  25450  ovolctb  25532  itg2monolem1  25792  itg2monolem2  25793  itg2monolem3  25794  itg2mono  25795  dvres  25953  dvres3a  25956  dvnff  25965  dvcmulf  25987  dvmptcl  26001  dvmptco  26014  dvlipcn  26036  dvgt0lem1  26044  itgsubstlem  26090  itgpowd  26092  dgrlem  26269  taylthlem1  26413  ulmval  26420  lgsfcl3  27359  midf  28922  grpodivf  30687  nvmf  30794  imsdf  30838  ipf  30862  0oo  30938  hoaddcl  31907  homulcl  31908  hosubcl  31922  fmptcof2  32809  ofoprabco  32816  fpwrelmap  32885  indf1ofs  33005  fedgmullem1  33887  sitmf  34610  fibp1  34659  ccatmulgnn0dir  34800  reprsuc  34873  pfxwlk  35438  cvmliftlem6  35604  cvmliftlem10  35608  mrsubff  35826  msubff  35844  tailf  36699  curf  38061  uncf  38062  poimirlem24  38107  ftc1anclem3  38158  rrnmet  38292  tendoplcl  41369  tendoicl  41384  intlewftc  42642  aks6d1c2  42711  aks6d1c6lem3  42753  pw2f1ocnv  43578  seff  44849  expgrowth  44875  dvnmul  46481  dvnprodlem2  46485  dvnprodlem3  46486  voliooicof  46534  stoweidlem34  46572  stoweidlem42  46580  stoweidlem48  46586  dirkerf  46635  fourierdlem41  46686  fourierdlem51  46695  fourierdlem57  46701  fourierdlem60  46704  fourierdlem61  46705  fourierdlem73  46717  fourierdlem75  46719  fourierdlem103  46747  fourierdlem104  46748  etransclem1  46773  etransclem2  46774  etransclem20  46792  etransclem33  46805  etransclem46  46818  sge0isum  46965  sge0seq  46984  isomenndlem  47068  ovnf  47101  ovnsubaddlem1  47108  hsphoif  47114  hoidmvlelem2  47134  hoidmvlelem3  47135  ovnhoilem1  47139  ovnhoilem2  47140  ovncvr2  47149  hoidifhspf  47156  hspmbllem2  47165  iccvonmbllem  47216  vonioolem1  47218  vonioolem2  47219  vonicclem1  47221  vonicclem2  47222  smfsupdmmbllem  47382  smfinfdmmbllem  47386  fsetsniunop  47607  1hegrlfgr  48718  funcringcsetcALTV2lem3  48878  funcringcsetcALTV2lem9  48884  funcringcsetclem3ALTV  48901  funcringcsetclem9ALTV  48907  fdivmptf  49127  refdivmptf  49128  itcovalendof  49255  ackendofnn0  49270  fucoppcid  49993  functermc  50093