Theorem feq1d 6644

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  feq1dd  6645  feq12d  6650  fco2  6688  fssres2  6702  fresin  6703  fresaun  6705  fmpt3d  7062  fressnfv  7107  f2ndf  8063  eroprf  8755  pmresg  8811  pw2f1olem  9012  ordtypelem4  9429  canthp1lem2  10567  fseq1p1m1  13543  repsf  14726  rlimres  15511  lo1res  15512  vdwapf  16934  fsets  17130  mrcf  17566  cofucl  17846  funcres  17854  funcestrcsetclem9  18105  1stfcl  18154  2ndfcl  18155  evlfcl  18179  yonedalem4c  18234  pmtrfinv  19427  pmtrff1o  19429  pmtrfcnv  19430  efgtf  19688  gsumzres  19875  isphld  21644  pjf  21703  frlmup1  21788  psrass1lem  21922  coe1f2  22183  lmbr  23233  tsmsres  24119  prdsdsf  24342  imasdsf1olem  24348  blfps  24381  blf  24382  tngngp2  24627  rrxmet  25385  ovolctb  25467  itg2monolem1  25727  itg2monolem2  25728  itg2monolem3  25729  itg2mono  25730  dvres  25888  dvres3a  25891  dvnff  25900  dvcmulf  25922  dvmptcl  25936  dvmptco  25949  dvlipcn  25971  dvgt0lem1  25979  itgsubstlem  26025  itgpowd  26027  dgrlem  26204  taylthlem1  26350  ulmval  26358  lgsfcl3  27295  midf  28858  grpodivf  30624  nvmf  30731  imsdf  30775  ipf  30799  0oo  30875  hoaddcl  31844  homulcl  31845  hosubcl  31859  fmptcof2  32745  ofoprabco  32752  fpwrelmap  32821  indf1ofs  32941  fedgmullem1  33789  sitmf  34512  fibp1  34561  ccatmulgnn0dir  34702  reprsuc  34775  pfxwlk  35322  cvmliftlem6  35488  cvmliftlem10  35492  mrsubff  35710  msubff  35728  tailf  36573  curf  37933  uncf  37934  poimirlem24  37979  ftc1anclem3  38030  rrnmet  38164  tendoplcl  41241  tendoicl  41256  intlewftc  42514  aks6d1c2  42583  aks6d1c6lem3  42625  pw2f1ocnv  43483  seff  44754  expgrowth  44780  dvnmul  46389  dvnprodlem2  46393  dvnprodlem3  46394  voliooicof  46442  stoweidlem34  46480  stoweidlem42  46488  stoweidlem48  46494  dirkerf  46543  fourierdlem41  46594  fourierdlem51  46603  fourierdlem57  46609  fourierdlem60  46612  fourierdlem61  46613  fourierdlem73  46625  fourierdlem75  46627  fourierdlem103  46655  fourierdlem104  46656  etransclem1  46681  etransclem2  46682  etransclem20  46700  etransclem33  46713  etransclem46  46726  sge0isum  46873  sge0seq  46892  isomenndlem  46976  ovnf  47009  ovnsubaddlem1  47016  hsphoif  47022  hoidmvlelem2  47042  hoidmvlelem3  47043  ovnhoilem1  47047  ovnhoilem2  47048  ovncvr2  47057  hoidifhspf  47064  hspmbllem2  47073  iccvonmbllem  47124  vonioolem1  47126  vonioolem2  47127  vonicclem1  47129  vonicclem2  47130  smfsupdmmbllem  47290  smfinfdmmbllem  47294  fsetsniunop  47509  1hegrlfgr  48620  funcringcsetcALTV2lem3  48780  funcringcsetcALTV2lem9  48786  funcringcsetclem3ALTV  48803  funcringcsetclem9ALTV  48809  fdivmptf  49029  refdivmptf  49030  itcovalendof  49157  ackendofnn0  49172  fucoppcid  49895  functermc  49995