Theorem feq1d 6689

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  feq1dd  6690  feq12d  6695  fco2  6734  fssres2  6748  fresin  6749  fresaun  6751  fmpt3d  7113  fressnfv  7159  f2ndf  8116  eroprf  8814  pmresg  8869  pw2f1olem  9070  ordtypelem4  9484  canthp1lem2  10639  fseq1p1m1  13628  repsf  14812  rlimres  15611  lo1res  15612  vdwapf  17033  fsets  17230  mrcf  17666  cofucl  17946  funcres  17954  funcestrcsetclem9  18205  1stfcl  18254  2ndfcl  18255  evlfcl  18279  yonedalem4c  18334  pmtrfinv  19532  pmtrff1o  19534  pmtrfcnv  19535  efgtf  19793  gsumzres  19980  isphld  21785  pjf  21844  frlmup1  21929  psrass1lem  22064  coe1f2  22350  lmbr  23396  tsmsres  24282  prdsdsf  24505  imasdsf1olem  24511  blfps  24544  blf  24545  tngngp2  24790  rrxmet  25548  ovolctb  25630  itg2monolem1  25890  itg2monolem2  25891  itg2monolem3  25892  itg2mono  25893  dvres  26051  dvres3a  26054  dvnff  26063  dvcmulf  26085  dvmptcl  26099  dvmptco  26112  dvlipcn  26134  dvgt0lem1  26142  itgsubstlem  26188  itgpowd  26190  dgrlem  26367  taylthlem1  26517  ulmval  26524  lgsfcl3  27463  midf  29066  grpodivf  30871  nvmf  30978  imsdf  31022  ipf  31046  0oo  31122  hoaddcl  32091  homulcl  32092  hosubcl  32106  fmptcof2  32983  ofoprabco  32990  fpwrelmap  33059  indf1ofs  33167  fedgmullem1  34000  sitmf  34723  fibp1  34772  ccatmulgnn0dir  34913  reprsuc  34983  pfxwlk  35597  cvmliftlem6  35763  cvmliftlem10  35767  mrsubff  35985  msubff  36003  tailf  36867  curf  38230  uncf  38231  poimirlem24  38276  ftc1anclem3  38327  rrnmet  38461  tendoplcl  41536  tendoicl  41551  intlewftc  42809  aks6d1c2  42878  aks6d1c6lem3  42920  pw2f1ocnv  43747  seff  45002  expgrowth  45028  dvnmul  46640  dvnprodlem2  46644  dvnprodlem3  46645  voliooicof  46693  stoweidlem34  46731  stoweidlem42  46739  stoweidlem48  46745  dirkerf  46794  fourierdlem41  46845  fourierdlem51  46854  fourierdlem57  46860  fourierdlem60  46863  fourierdlem61  46864  fourierdlem73  46876  fourierdlem75  46878  fourierdlem103  46906  fourierdlem104  46907  etransclem1  46932  etransclem2  46933  etransclem20  46951  etransclem33  46964  etransclem46  46977  sge0isum  47124  sge0seq  47143  isomenndlem  47227  ovnf  47260  ovnsubaddlem1  47267  hsphoif  47273  hoidmvlelem2  47293  hoidmvlelem3  47294  ovnhoilem1  47298  ovnhoilem2  47299  ovncvr2  47308  hoidifhspf  47315  hspmbllem2  47324  iccvonmbllem  47375  vonioolem1  47377  vonioolem2  47378  vonicclem1  47380  vonicclem2  47381  smfsupdmmbllem  47541  smfinfdmmbllem  47545  fsetsniunop  47769  1hegrlfgr  48880  funcringcsetcALTV2lem3  49040  funcringcsetcALTV2lem9  49046  funcringcsetclem3ALTV  49063  funcringcsetclem9ALTV  49069  fdivmptf  49304  refdivmptf  49305  itcovalendof  49432  ackendofnn0  49447  fucoppcid  50169  functermc  50269