Theorem feq1d 6501

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ⟶wf 6353

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-fun 6359  df-fn 6360  df-f 6361

This theorem is referenced by:  feq12d  6504  fco2  6535  fssres2  6548  fresin  6549  fresaun  6551  fmpt3d  6882  fressnfv  6924  f2ndf  7818  eroprf  8397  pmresg  8436  pw2f1olem  8623  ordtypelem4  8987  canthp1lem2  10077  fseq1p1m1  12984  repsf  14137  rlimres  14917  lo1res  14918  vdwapf  16310  fsets  16518  mrcf  16882  cofucl  17160  funcres  17168  funcestrcsetclem9  17400  1stfcl  17449  2ndfcl  17450  evlfcl  17474  yonedalem4c  17529  pmtrfinv  18591  pmtrff1o  18593  pmtrfcnv  18594  efgtf  18850  gsumzres  19031  psrass1lem  20159  coe1f2  20379  isphld  20800  pjf  20859  frlmup1  20944  lmbr  21868  tsmsres  22754  prdsdsf  22979  imasdsf1olem  22985  blfps  23018  blf  23019  tngngp2  23263  rrxmet  24013  ovolctb  24093  itg2monolem1  24353  itg2monolem2  24354  itg2monolem3  24355  itg2mono  24356  dvres  24511  dvres3a  24514  dvnff  24522  dvcmulf  24544  dvmptcl  24558  dvmptco  24571  dvlipcn  24593  dvgt0lem1  24601  itgsubstlem  24647  dgrlem  24821  taylthlem1  24963  ulmval  24970  lgsfcl3  25896  midf  26564  grpodivf  28317  nvmf  28424  imsdf  28468  ipf  28492  0oo  28568  hoaddcl  29537  homulcl  29538  hosubcl  29552  fmptcof2  30404  ofoprabco  30411  fpwrelmap  30471  fedgmullem1  31027  indf1ofs  31287  sitmf  31612  fibp1  31661  ccatmulgnn0dir  31814  reprsuc  31888  pfxwlk  32372  cvmliftlem6  32539  cvmliftlem10  32543  mrsubff  32761  msubff  32779  tailf  33725  curf  34872  uncf  34873  poimirlem24  34918  ftc1anclem3  34971  rrnmet  35109  tendoplcl  37919  tendoicl  37934  pw2f1ocnv  39641  itgpowd  39828  seff  40648  expgrowth  40674  feq1dd  41430  dvnmul  42235  dvnprodlem2  42239  dvnprodlem3  42240  voliooicof  42288  stoweidlem34  42326  stoweidlem42  42334  stoweidlem48  42340  dirkerf  42389  fourierdlem41  42440  fourierdlem51  42449  fourierdlem57  42455  fourierdlem60  42458  fourierdlem61  42459  fourierdlem73  42471  fourierdlem75  42473  fourierdlem103  42501  fourierdlem104  42502  etransclem1  42527  etransclem2  42528  etransclem20  42546  etransclem33  42559  etransclem46  42572  sge0isum  42716  sge0seq  42735  isomenndlem  42819  hoicvr  42837  ovnf  42852  ovnsubaddlem1  42859  hsphoif  42865  hoidmvlelem2  42885  hoidmvlelem3  42886  ovnhoilem1  42890  ovnhoilem2  42891  ovncvr2  42900  hoidifhspf  42907  hspmbllem2  42916  iccvonmbllem  42967  vonioolem1  42969  vonioolem2  42970  vonicclem1  42972  vonicclem2  42973  1hegrlfgr  44014  funcringcsetcALTV2lem3  44316  funcringcsetcALTV2lem9  44322  funcringcsetclem3ALTV  44339  funcringcsetclem9ALTV  44345  fdivmptf  44608  refdivmptf  44609