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 207   = wceq 1547  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  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  7064  fressnfv  7110  f2ndf  8066  eroprf  8759  pmresg  8815  pw2f1olem  9016  ordtypelem4  9433  canthp1lem2  10574  fseq1p1m1  13550  repsf  14733  rlimres  15518  lo1res  15519  vdwapf  16941  fsets  17137  mrcf  17573  cofucl  17853  funcres  17861  funcestrcsetclem9  18112  1stfcl  18161  2ndfcl  18162  evlfcl  18186  yonedalem4c  18241  pmtrfinv  19434  pmtrff1o  19436  pmtrfcnv  19437  efgtf  19695  gsumzres  19882  isphld  21636  pjf  21695  frlmup1  21780  psrass1lem  21915  coe1f2  22201  lmbr  23248  tsmsres  24134  prdsdsf  24357  imasdsf1olem  24363  blfps  24396  blf  24397  tngngp2  24642  rrxmet  25400  ovolctb  25482  itg2monolem1  25742  itg2monolem2  25743  itg2monolem3  25744  itg2mono  25745  dvres  25903  dvres3a  25906  dvnff  25915  dvcmulf  25937  dvmptcl  25951  dvmptco  25964  dvlipcn  25986  dvgt0lem1  25994  itgsubstlem  26040  itgpowd  26042  dgrlem  26219  taylthlem1  26363  ulmval  26370  lgsfcl3  27306  midf  28869  grpodivf  30634  nvmf  30741  imsdf  30785  ipf  30809  0oo  30885  hoaddcl  31854  homulcl  31855  hosubcl  31869  fmptcof2  32756  ofoprabco  32763  fpwrelmap  32832  indf1ofs  32952  fedgmullem1  33820  sitmf  34543  fibp1  34592  ccatmulgnn0dir  34733  reprsuc  34806  pfxwlk  35359  cvmliftlem6  35525  cvmliftlem10  35529  mrsubff  35747  msubff  35765  tailf  36610  curf  37972  uncf  37973  poimirlem24  38018  ftc1anclem3  38069  rrnmet  38203  tendoplcl  41280  tendoicl  41295  intlewftc  42553  aks6d1c2  42622  aks6d1c6lem3  42664  pw2f1ocnv  43489  seff  44760  expgrowth  44786  dvnmul  46393  dvnprodlem2  46397  dvnprodlem3  46398  voliooicof  46446  stoweidlem34  46484  stoweidlem42  46492  stoweidlem48  46498  dirkerf  46547  fourierdlem41  46598  fourierdlem51  46607  fourierdlem57  46613  fourierdlem60  46616  fourierdlem61  46617  fourierdlem73  46629  fourierdlem75  46631  fourierdlem103  46659  fourierdlem104  46660  etransclem1  46685  etransclem2  46686  etransclem20  46704  etransclem33  46717  etransclem46  46730  sge0isum  46877  sge0seq  46896  isomenndlem  46980  ovnf  47013  ovnsubaddlem1  47020  hsphoif  47026  hoidmvlelem2  47046  hoidmvlelem3  47047  ovnhoilem1  47051  ovnhoilem2  47052  ovncvr2  47061  hoidifhspf  47068  hspmbllem2  47077  iccvonmbllem  47128  vonioolem1  47130  vonioolem2  47131  vonicclem1  47133  vonicclem2  47134  smfsupdmmbllem  47294  smfinfdmmbllem  47298  fsetsniunop  47519  1hegrlfgr  48630  funcringcsetcALTV2lem3  48790  funcringcsetcALTV2lem9  48796  funcringcsetclem3ALTV  48813  funcringcsetclem9ALTV  48819  fdivmptf  49039  refdivmptf  49040  itcovalendof  49167  ackendofnn0  49182  fucoppcid  49905  functermc  50005