Theorem feq1d 6732

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-fun 6575  df-fn 6576  df-f 6577

This theorem is referenced by:  feq12d  6735  fco2  6774  fssres2  6789  fresin  6790  fresaun  6792  fmpt3d  7150  fressnfv  7194  f2ndf  8161  eroprf  8873  pmresg  8928  pw2f1olem  9142  ordtypelem4  9590  canthp1lem2  10722  fseq1p1m1  13658  repsf  14821  rlimres  15604  lo1res  15605  vdwapf  17019  fsets  17216  mrcf  17667  cofucl  17952  funcres  17960  funcestrcsetclem9  18217  1stfcl  18266  2ndfcl  18267  evlfcl  18292  yonedalem4c  18347  pmtrfinv  19503  pmtrff1o  19505  pmtrfcnv  19506  efgtf  19764  gsumzres  19951  isphld  21695  pjf  21756  frlmup1  21841  psrass1lem  21975  coe1f2  22232  lmbr  23287  tsmsres  24173  prdsdsf  24398  imasdsf1olem  24404  blfps  24437  blf  24438  tngngp2  24694  rrxmet  25461  ovolctb  25544  itg2monolem1  25805  itg2monolem2  25806  itg2monolem3  25807  itg2mono  25808  dvres  25966  dvres3a  25969  dvnff  25979  dvcmulf  26002  dvmptcl  26017  dvmptco  26030  dvlipcn  26053  dvgt0lem1  26061  itgsubstlem  26109  itgpowd  26111  dgrlem  26288  taylthlem1  26433  ulmval  26441  lgsfcl3  27380  midf  28802  grpodivf  30570  nvmf  30677  imsdf  30721  ipf  30745  0oo  30821  hoaddcl  31790  homulcl  31791  hosubcl  31805  fmptcof2  32675  ofoprabco  32682  fpwrelmap  32747  fedgmullem1  33642  indf1ofs  33990  sitmf  34317  fibp1  34366  ccatmulgnn0dir  34519  reprsuc  34592  pfxwlk  35091  cvmliftlem6  35258  cvmliftlem10  35262  mrsubff  35480  msubff  35498  tailf  36341  curf  37558  uncf  37559  poimirlem24  37604  ftc1anclem3  37655  rrnmet  37789  tendoplcl  40738  tendoicl  40753  intlewftc  42018  aks6d1c2  42087  aks6d1c6lem3  42129  pw2f1ocnv  42994  seff  44278  expgrowth  44304  feq1dd  45074  dvnmul  45864  dvnprodlem2  45868  dvnprodlem3  45869  voliooicof  45917  stoweidlem34  45955  stoweidlem42  45963  stoweidlem48  45969  dirkerf  46018  fourierdlem41  46069  fourierdlem51  46078  fourierdlem57  46084  fourierdlem60  46087  fourierdlem61  46088  fourierdlem73  46100  fourierdlem75  46102  fourierdlem103  46130  fourierdlem104  46131  etransclem1  46156  etransclem2  46157  etransclem20  46175  etransclem33  46188  etransclem46  46201  sge0isum  46348  sge0seq  46367  isomenndlem  46451  hoicvr  46469  ovnf  46484  ovnsubaddlem1  46491  hsphoif  46497  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoilem1  46522  ovnhoilem2  46523  ovncvr2  46532  hoidifhspf  46539  hspmbllem2  46548  iccvonmbllem  46599  vonioolem1  46601  vonioolem2  46602  vonicclem1  46604  vonicclem2  46605  smfsupdmmbllem  46765  smfinfdmmbllem  46769  fsetsniunop  46964  1hegrlfgr  47855  funcringcsetcALTV2lem3  48015  funcringcsetcALTV2lem9  48021  funcringcsetclem3ALTV  48038  funcringcsetclem9ALTV  48044  fdivmptf  48275  refdivmptf  48276  itcovalendof  48403  ackendofnn0  48418