Theorem feq1d 6650

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6500  df-fn 6501  df-f 6502

This theorem is referenced by:  feq1dd  6651  feq12d  6656  fco2  6694  fssres2  6708  fresin  6709  fresaun  6711  fmpt3d  7068  fressnfv  7114  f2ndf  8070  eroprf  8762  pmresg  8818  pw2f1olem  9019  ordtypelem4  9436  canthp1lem2  10576  fseq1p1m1  13552  repsf  14735  rlimres  15520  lo1res  15521  vdwapf  16943  fsets  17139  mrcf  17575  cofucl  17855  funcres  17863  funcestrcsetclem9  18114  1stfcl  18163  2ndfcl  18164  evlfcl  18188  yonedalem4c  18243  pmtrfinv  19436  pmtrff1o  19438  pmtrfcnv  19439  efgtf  19697  gsumzres  19884  isphld  21634  pjf  21693  frlmup1  21778  psrass1lem  21912  coe1f2  22173  lmbr  23223  tsmsres  24109  prdsdsf  24332  imasdsf1olem  24338  blfps  24371  blf  24372  tngngp2  24617  rrxmet  25375  ovolctb  25457  itg2monolem1  25717  itg2monolem2  25718  itg2monolem3  25719  itg2mono  25720  dvres  25878  dvres3a  25881  dvnff  25890  dvcmulf  25912  dvmptcl  25926  dvmptco  25939  dvlipcn  25961  dvgt0lem1  25969  itgsubstlem  26015  itgpowd  26017  dgrlem  26194  taylthlem1  26338  ulmval  26345  lgsfcl3  27281  midf  28844  grpodivf  30609  nvmf  30716  imsdf  30760  ipf  30784  0oo  30860  hoaddcl  31829  homulcl  31830  hosubcl  31844  fmptcof2  32730  ofoprabco  32737  fpwrelmap  32806  indf1ofs  32926  fedgmullem1  33773  sitmf  34496  fibp1  34545  ccatmulgnn0dir  34686  reprsuc  34759  pfxwlk  35306  cvmliftlem6  35472  cvmliftlem10  35476  mrsubff  35694  msubff  35712  tailf  36557  curf  37919  uncf  37920  poimirlem24  37965  ftc1anclem3  38016  rrnmet  38150  tendoplcl  41227  tendoicl  41242  intlewftc  42500  aks6d1c2  42569  aks6d1c6lem3  42611  pw2f1ocnv  43465  seff  44736  expgrowth  44762  dvnmul  46371  dvnprodlem2  46375  dvnprodlem3  46376  voliooicof  46424  stoweidlem34  46462  stoweidlem42  46470  stoweidlem48  46476  dirkerf  46525  fourierdlem41  46576  fourierdlem51  46585  fourierdlem57  46591  fourierdlem60  46594  fourierdlem61  46595  fourierdlem73  46607  fourierdlem75  46609  fourierdlem103  46637  fourierdlem104  46638  etransclem1  46663  etransclem2  46664  etransclem20  46682  etransclem33  46695  etransclem46  46708  sge0isum  46855  sge0seq  46874  isomenndlem  46958  ovnf  46991  ovnsubaddlem1  46998  hsphoif  47004  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem1  47029  ovnhoilem2  47030  ovncvr2  47039  hoidifhspf  47046  hspmbllem2  47055  iccvonmbllem  47106  vonioolem1  47108  vonioolem2  47109  vonicclem1  47111  vonicclem2  47112  smfsupdmmbllem  47272  smfinfdmmbllem  47276  fsetsniunop  47497  1hegrlfgr  48608  funcringcsetcALTV2lem3  48768  funcringcsetcALTV2lem9  48774  funcringcsetclem3ALTV  48791  funcringcsetclem9ALTV  48797  fdivmptf  49017  refdivmptf  49018  itcovalendof  49145  ackendofnn0  49160  fucoppcid  49883  functermc  49983