Theorem feq1d 6638

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  feq1dd  6639  feq12d  6644  fco2  6682  fssres2  6696  fresin  6697  fresaun  6699  fmpt3d  7054  fressnfv  7098  f2ndf  8060  eroprf  8749  pmresg  8804  pw2f1olem  9005  ordtypelem4  9432  canthp1lem2  10566  fseq1p1m1  13519  repsf  14697  rlimres  15483  lo1res  15484  vdwapf  16902  fsets  17098  mrcf  17533  cofucl  17813  funcres  17821  funcestrcsetclem9  18072  1stfcl  18121  2ndfcl  18122  evlfcl  18146  yonedalem4c  18201  pmtrfinv  19358  pmtrff1o  19360  pmtrfcnv  19361  efgtf  19619  gsumzres  19806  isphld  21579  pjf  21638  frlmup1  21723  psrass1lem  21857  coe1f2  22110  lmbr  23161  tsmsres  24047  prdsdsf  24271  imasdsf1olem  24277  blfps  24310  blf  24311  tngngp2  24556  rrxmet  25324  ovolctb  25407  itg2monolem1  25667  itg2monolem2  25668  itg2monolem3  25669  itg2mono  25670  dvres  25828  dvres3a  25831  dvnff  25841  dvcmulf  25864  dvmptcl  25879  dvmptco  25892  dvlipcn  25915  dvgt0lem1  25923  itgsubstlem  25971  itgpowd  25973  dgrlem  26150  taylthlem1  26297  ulmval  26305  lgsfcl3  27245  midf  28739  grpodivf  30500  nvmf  30607  imsdf  30651  ipf  30675  0oo  30751  hoaddcl  31720  homulcl  31721  hosubcl  31735  fmptcof2  32614  ofoprabco  32621  fpwrelmap  32689  indf1ofs  32822  fedgmullem1  33601  sitmf  34319  fibp1  34368  ccatmulgnn0dir  34509  reprsuc  34582  pfxwlk  35096  cvmliftlem6  35262  cvmliftlem10  35266  mrsubff  35484  msubff  35502  tailf  36348  curf  37577  uncf  37578  poimirlem24  37623  ftc1anclem3  37674  rrnmet  37808  tendoplcl  40760  tendoicl  40775  intlewftc  42034  aks6d1c2  42103  aks6d1c6lem3  42145  pw2f1ocnv  43010  seff  44282  expgrowth  44308  dvnmul  45925  dvnprodlem2  45929  dvnprodlem3  45930  voliooicof  45978  stoweidlem34  46016  stoweidlem42  46024  stoweidlem48  46030  dirkerf  46079  fourierdlem41  46130  fourierdlem51  46139  fourierdlem57  46145  fourierdlem60  46148  fourierdlem61  46149  fourierdlem73  46161  fourierdlem75  46163  fourierdlem103  46191  fourierdlem104  46192  etransclem1  46217  etransclem2  46218  etransclem20  46236  etransclem33  46249  etransclem46  46262  sge0isum  46409  sge0seq  46428  isomenndlem  46512  hoicvr  46530  ovnf  46545  ovnsubaddlem1  46552  hsphoif  46558  hoidmvlelem2  46578  hoidmvlelem3  46579  ovnhoilem1  46583  ovnhoilem2  46584  ovncvr2  46593  hoidifhspf  46600  hspmbllem2  46609  iccvonmbllem  46660  vonioolem1  46662  vonioolem2  46663  vonicclem1  46665  vonicclem2  46666  smfsupdmmbllem  46826  smfinfdmmbllem  46830  fsetsniunop  47034  1hegrlfgr  48117  funcringcsetcALTV2lem3  48277  funcringcsetcALTV2lem9  48283  funcringcsetclem3ALTV  48300  funcringcsetclem9ALTV  48306  fdivmptf  48527  refdivmptf  48528  itcovalendof  48655  ackendofnn0  48670  fucoppcid  49394  functermc  49494