Theorem feq1d 6652

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

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  feq1dd  6653  feq12d  6658  fco2  6696  fssres2  6710  fresin  6711  fresaun  6713  fmpt3d  7070  fressnfv  7115  f2ndf  8072  eroprf  8764  pmresg  8820  pw2f1olem  9021  ordtypelem4  9438  canthp1lem2  10576  fseq1p1m1  13526  repsf  14708  rlimres  15493  lo1res  15494  vdwapf  16912  fsets  17108  mrcf  17544  cofucl  17824  funcres  17832  funcestrcsetclem9  18083  1stfcl  18132  2ndfcl  18133  evlfcl  18157  yonedalem4c  18212  pmtrfinv  19402  pmtrff1o  19404  pmtrfcnv  19405  efgtf  19663  gsumzres  19850  isphld  21621  pjf  21680  frlmup1  21765  psrass1lem  21900  coe1f2  22162  lmbr  23214  tsmsres  24100  prdsdsf  24323  imasdsf1olem  24329  blfps  24362  blf  24363  tngngp2  24608  rrxmet  25376  ovolctb  25459  itg2monolem1  25719  itg2monolem2  25720  itg2monolem3  25721  itg2mono  25722  dvres  25880  dvres3a  25883  dvnff  25893  dvcmulf  25916  dvmptcl  25931  dvmptco  25944  dvlipcn  25967  dvgt0lem1  25975  itgsubstlem  26023  itgpowd  26025  dgrlem  26202  taylthlem1  26349  ulmval  26357  lgsfcl3  27297  midf  28860  grpodivf  30625  nvmf  30732  imsdf  30776  ipf  30800  0oo  30876  hoaddcl  31845  homulcl  31846  hosubcl  31860  fmptcof2  32746  ofoprabco  32753  fpwrelmap  32822  indf1ofs  32958  fedgmullem1  33806  sitmf  34529  fibp1  34578  ccatmulgnn0dir  34719  reprsuc  34792  pfxwlk  35337  cvmliftlem6  35503  cvmliftlem10  35507  mrsubff  35725  msubff  35743  tailf  36588  curf  37843  uncf  37844  poimirlem24  37889  ftc1anclem3  37940  rrnmet  38074  tendoplcl  41151  tendoicl  41166  intlewftc  42425  aks6d1c2  42494  aks6d1c6lem3  42536  pw2f1ocnv  43388  seff  44659  expgrowth  44685  dvnmul  46295  dvnprodlem2  46299  dvnprodlem3  46300  voliooicof  46348  stoweidlem34  46386  stoweidlem42  46394  stoweidlem48  46400  dirkerf  46449  fourierdlem41  46500  fourierdlem51  46509  fourierdlem57  46515  fourierdlem60  46518  fourierdlem61  46519  fourierdlem73  46531  fourierdlem75  46533  fourierdlem103  46561  fourierdlem104  46562  etransclem1  46587  etransclem2  46588  etransclem20  46606  etransclem33  46619  etransclem46  46632  sge0isum  46779  sge0seq  46798  isomenndlem  46882  hoicvr  46900  ovnf  46915  ovnsubaddlem1  46922  hsphoif  46928  hoidmvlelem2  46948  hoidmvlelem3  46949  ovnhoilem1  46953  ovnhoilem2  46954  ovncvr2  46963  hoidifhspf  46970  hspmbllem2  46979  iccvonmbllem  47030  vonioolem1  47032  vonioolem2  47033  vonicclem1  47035  vonicclem2  47036  smfsupdmmbllem  47196  smfinfdmmbllem  47200  fsetsniunop  47403  1hegrlfgr  48486  funcringcsetcALTV2lem3  48646  funcringcsetcALTV2lem9  48652  funcringcsetclem3ALTV  48669  funcringcsetclem9ALTV  48675  fdivmptf  48895  refdivmptf  48896  itcovalendof  49023  ackendofnn0  49038  fucoppcid  49761  functermc  49861