Theorem feq1d 6720

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-fun 6564  df-fn 6565  df-f 6566

This theorem is referenced by:  feq1dd  6721  feq12d  6724  fco2  6762  fssres2  6776  fresin  6777  fresaun  6779  fmpt3d  7135  fressnfv  7179  f2ndf  8143  eroprf  8853  pmresg  8908  pw2f1olem  9114  ordtypelem4  9558  canthp1lem2  10690  fseq1p1m1  13634  repsf  14807  rlimres  15590  lo1res  15591  vdwapf  17005  fsets  17202  mrcf  17653  cofucl  17938  funcres  17946  funcestrcsetclem9  18203  1stfcl  18252  2ndfcl  18253  evlfcl  18278  yonedalem4c  18333  pmtrfinv  19493  pmtrff1o  19495  pmtrfcnv  19496  efgtf  19754  gsumzres  19941  isphld  21689  pjf  21750  frlmup1  21835  psrass1lem  21969  coe1f2  22226  lmbr  23281  tsmsres  24167  prdsdsf  24392  imasdsf1olem  24398  blfps  24431  blf  24432  tngngp2  24688  rrxmet  25455  ovolctb  25538  itg2monolem1  25799  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  dvres  25960  dvres3a  25963  dvnff  25973  dvcmulf  25996  dvmptcl  26011  dvmptco  26024  dvlipcn  26047  dvgt0lem1  26055  itgsubstlem  26103  itgpowd  26105  dgrlem  26282  taylthlem1  26429  ulmval  26437  lgsfcl3  27376  midf  28798  grpodivf  30566  nvmf  30673  imsdf  30717  ipf  30741  0oo  30817  hoaddcl  31786  homulcl  31787  hosubcl  31801  fmptcof2  32673  ofoprabco  32680  fpwrelmap  32750  fedgmullem1  33656  indf1ofs  34006  sitmf  34333  fibp1  34382  ccatmulgnn0dir  34535  reprsuc  34608  pfxwlk  35107  cvmliftlem6  35274  cvmliftlem10  35278  mrsubff  35496  msubff  35514  tailf  36357  curf  37584  uncf  37585  poimirlem24  37630  ftc1anclem3  37681  rrnmet  37815  tendoplcl  40763  tendoicl  40778  intlewftc  42042  aks6d1c2  42111  aks6d1c6lem3  42153  pw2f1ocnv  43025  seff  44304  expgrowth  44330  dvnmul  45898  dvnprodlem2  45902  dvnprodlem3  45903  voliooicof  45951  stoweidlem34  45989  stoweidlem42  45997  stoweidlem48  46003  dirkerf  46052  fourierdlem41  46103  fourierdlem51  46112  fourierdlem57  46118  fourierdlem60  46121  fourierdlem61  46122  fourierdlem73  46134  fourierdlem75  46136  fourierdlem103  46164  fourierdlem104  46165  etransclem1  46190  etransclem2  46191  etransclem20  46209  etransclem33  46222  etransclem46  46235  sge0isum  46382  sge0seq  46401  isomenndlem  46485  hoicvr  46503  ovnf  46518  ovnsubaddlem1  46525  hsphoif  46531  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoilem1  46556  ovnhoilem2  46557  ovncvr2  46566  hoidifhspf  46573  hspmbllem2  46582  iccvonmbllem  46633  vonioolem1  46635  vonioolem2  46636  vonicclem1  46638  vonicclem2  46639  smfsupdmmbllem  46799  smfinfdmmbllem  46803  fsetsniunop  46998  1hegrlfgr  47975  funcringcsetcALTV2lem3  48135  funcringcsetcALTV2lem9  48141  funcringcsetclem3ALTV  48158  funcringcsetclem9ALTV  48164  fdivmptf  48390  refdivmptf  48391  itcovalendof  48518  ackendofnn0  48533