Theorem feq1d 6713

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  ⟶wf 6550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-br 5154  df-opab 5216  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-fun 6556  df-fn 6557  df-f 6558

This theorem is referenced by:  feq12d  6716  fco2  6755  fssres2  6770  fresin  6771  fresaun  6773  fmpt3d  7130  fressnfv  7174  f2ndf  8134  eroprf  8844  pmresg  8899  pw2f1olem  9114  ordtypelem4  9564  canthp1lem2  10696  fseq1p1m1  13629  repsf  14781  rlimres  15560  lo1res  15561  vdwapf  16974  fsets  17171  mrcf  17622  cofucl  17907  funcres  17915  funcestrcsetclem9  18172  1stfcl  18221  2ndfcl  18222  evlfcl  18247  yonedalem4c  18302  pmtrfinv  19459  pmtrff1o  19461  pmtrfcnv  19462  efgtf  19720  gsumzres  19907  isphld  21650  pjf  21711  frlmup1  21796  psrass1lemOLD  21938  psrass1lem  21941  coe1f2  22199  lmbr  23253  tsmsres  24139  prdsdsf  24364  imasdsf1olem  24370  blfps  24403  blf  24404  tngngp2  24660  rrxmet  25427  ovolctb  25510  itg2monolem1  25771  itg2monolem2  25772  itg2monolem3  25773  itg2mono  25774  dvres  25931  dvres3a  25934  dvnff  25944  dvcmulf  25967  dvmptcl  25982  dvmptco  25995  dvlipcn  26018  dvgt0lem1  26026  itgsubstlem  26074  itgpowd  26076  dgrlem  26256  taylthlem1  26401  ulmval  26409  lgsfcl3  27347  midf  28703  grpodivf  30471  nvmf  30578  imsdf  30622  ipf  30646  0oo  30722  hoaddcl  31691  homulcl  31692  hosubcl  31706  fmptcof2  32574  ofoprabco  32581  fpwrelmap  32647  fedgmullem1  33524  indf1ofs  33859  sitmf  34186  fibp1  34235  ccatmulgnn0dir  34388  reprsuc  34461  pfxwlk  34951  cvmliftlem6  35118  cvmliftlem10  35122  mrsubff  35340  msubff  35358  tailf  36087  curf  37299  uncf  37300  poimirlem24  37345  ftc1anclem3  37396  rrnmet  37530  tendoplcl  40480  tendoicl  40495  intlewftc  41760  aks6d1c2  41828  aks6d1c6lem3  41870  pw2f1ocnv  42695  seff  43983  expgrowth  44009  feq1dd  44774  dvnmul  45564  dvnprodlem2  45568  dvnprodlem3  45569  voliooicof  45617  stoweidlem34  45655  stoweidlem42  45663  stoweidlem48  45669  dirkerf  45718  fourierdlem41  45769  fourierdlem51  45778  fourierdlem57  45784  fourierdlem60  45787  fourierdlem61  45788  fourierdlem73  45800  fourierdlem75  45802  fourierdlem103  45830  fourierdlem104  45831  etransclem1  45856  etransclem2  45857  etransclem20  45875  etransclem33  45888  etransclem46  45901  sge0isum  46048  sge0seq  46067  isomenndlem  46151  hoicvr  46169  ovnf  46184  ovnsubaddlem1  46191  hsphoif  46197  hoidmvlelem2  46217  hoidmvlelem3  46218  ovnhoilem1  46222  ovnhoilem2  46223  ovncvr2  46232  hoidifhspf  46239  hspmbllem2  46248  iccvonmbllem  46299  vonioolem1  46301  vonioolem2  46302  vonicclem1  46304  vonicclem2  46305  smfsupdmmbllem  46465  smfinfdmmbllem  46469  fsetsniunop  46664  1hegrlfgr  47509  funcringcsetcALTV2lem3  47669  funcringcsetcALTV2lem9  47675  funcringcsetclem3ALTV  47692  funcringcsetclem9ALTV  47698  fdivmptf  47929  refdivmptf  47930  itcovalendof  48057  ackendofnn0  48072