Theorem feq1d 6638

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

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

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  feq1dd  6639  feq12d  6644  fco2  6682  fssres2  6696  fresin  6697  fresaun  6699  fmpt3d  7055  fressnfv  7099  f2ndf  8056  eroprf  8745  pmresg  8800  pw2f1olem  9001  ordtypelem4  9414  canthp1lem2  10551  fseq1p1m1  13500  repsf  14682  rlimres  15467  lo1res  15468  vdwapf  16886  fsets  17082  mrcf  17517  cofucl  17797  funcres  17805  funcestrcsetclem9  18056  1stfcl  18105  2ndfcl  18106  evlfcl  18130  yonedalem4c  18185  pmtrfinv  19375  pmtrff1o  19377  pmtrfcnv  19378  efgtf  19636  gsumzres  19823  isphld  21593  pjf  21652  frlmup1  21737  psrass1lem  21871  coe1f2  22123  lmbr  23174  tsmsres  24060  prdsdsf  24283  imasdsf1olem  24289  blfps  24322  blf  24323  tngngp2  24568  rrxmet  25336  ovolctb  25419  itg2monolem1  25679  itg2monolem2  25680  itg2monolem3  25681  itg2mono  25682  dvres  25840  dvres3a  25843  dvnff  25853  dvcmulf  25876  dvmptcl  25891  dvmptco  25904  dvlipcn  25927  dvgt0lem1  25935  itgsubstlem  25983  itgpowd  25985  dgrlem  26162  taylthlem1  26309  ulmval  26317  lgsfcl3  27257  midf  28755  grpodivf  30520  nvmf  30627  imsdf  30671  ipf  30695  0oo  30771  hoaddcl  31740  homulcl  31741  hosubcl  31755  fmptcof2  32641  ofoprabco  32648  fpwrelmap  32720  indf1ofs  32854  fedgmullem1  33663  sitmf  34386  fibp1  34435  ccatmulgnn0dir  34576  reprsuc  34649  pfxwlk  35189  cvmliftlem6  35355  cvmliftlem10  35359  mrsubff  35577  msubff  35595  tailf  36440  curf  37658  uncf  37659  poimirlem24  37704  ftc1anclem3  37755  rrnmet  37889  tendoplcl  40900  tendoicl  40915  intlewftc  42174  aks6d1c2  42243  aks6d1c6lem3  42285  pw2f1ocnv  43154  seff  44426  expgrowth  44452  dvnmul  46065  dvnprodlem2  46069  dvnprodlem3  46070  voliooicof  46118  stoweidlem34  46156  stoweidlem42  46164  stoweidlem48  46170  dirkerf  46219  fourierdlem41  46270  fourierdlem51  46279  fourierdlem57  46285  fourierdlem60  46288  fourierdlem61  46289  fourierdlem73  46301  fourierdlem75  46303  fourierdlem103  46331  fourierdlem104  46332  etransclem1  46357  etransclem2  46358  etransclem20  46376  etransclem33  46389  etransclem46  46402  sge0isum  46549  sge0seq  46568  isomenndlem  46652  hoicvr  46670  ovnf  46685  ovnsubaddlem1  46692  hsphoif  46698  hoidmvlelem2  46718  hoidmvlelem3  46719  ovnhoilem1  46723  ovnhoilem2  46724  ovncvr2  46733  hoidifhspf  46740  hspmbllem2  46749  iccvonmbllem  46800  vonioolem1  46802  vonioolem2  46803  vonicclem1  46805  vonicclem2  46806  smfsupdmmbllem  46966  smfinfdmmbllem  46970  fsetsniunop  47173  1hegrlfgr  48256  funcringcsetcALTV2lem3  48416  funcringcsetcALTV2lem9  48422  funcringcsetclem3ALTV  48439  funcringcsetclem9ALTV  48445  fdivmptf  48666  refdivmptf  48667  itcovalendof  48794  ackendofnn0  48809  fucoppcid  49533  functermc  49633