Theorem feq1d 6594

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ⟶wf 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-fun 6439  df-fn 6440  df-f 6441

This theorem is referenced by:  feq12d  6597  fco2  6636  fssres2  6651  fresin  6652  fresaun  6654  fmpt3d  6999  fressnfv  7041  f2ndf  7970  eroprf  8613  pmresg  8667  pw2f1olem  8872  ordtypelem4  9289  canthp1lem2  10418  fseq1p1m1  13339  repsf  14495  rlimres  15276  lo1res  15277  vdwapf  16682  fsets  16879  mrcf  17327  cofucl  17612  funcres  17620  funcestrcsetclem9  17874  1stfcl  17923  2ndfcl  17924  evlfcl  17949  yonedalem4c  18004  pmtrfinv  19078  pmtrff1o  19080  pmtrfcnv  19081  efgtf  19337  gsumzres  19519  isphld  20868  pjf  20929  frlmup1  21014  psrass1lemOLD  21152  psrass1lem  21155  coe1f2  21389  lmbr  22418  tsmsres  23304  prdsdsf  23529  imasdsf1olem  23535  blfps  23568  blf  23569  tngngp2  23825  rrxmet  24581  ovolctb  24663  itg2monolem1  24924  itg2monolem2  24925  itg2monolem3  24926  itg2mono  24927  dvres  25084  dvres3a  25087  dvnff  25096  dvcmulf  25118  dvmptcl  25132  dvmptco  25145  dvlipcn  25167  dvgt0lem1  25175  itgsubstlem  25221  itgpowd  25223  dgrlem  25399  taylthlem1  25541  ulmval  25548  lgsfcl3  26475  midf  27146  grpodivf  28909  nvmf  29016  imsdf  29060  ipf  29084  0oo  29160  hoaddcl  30129  homulcl  30130  hosubcl  30144  fmptcof2  31003  ofoprabco  31010  fpwrelmap  31077  fedgmullem1  31719  indf1ofs  32003  sitmf  32328  fibp1  32377  ccatmulgnn0dir  32530  reprsuc  32604  pfxwlk  33094  cvmliftlem6  33261  cvmliftlem10  33265  mrsubff  33483  msubff  33501  tailf  34573  curf  35764  uncf  35765  poimirlem24  35810  ftc1anclem3  35861  rrnmet  35996  tendoplcl  38802  tendoicl  38817  intlewftc  40076  pw2f1ocnv  40866  seff  41934  expgrowth  41960  feq1dd  42710  dvnmul  43491  dvnprodlem2  43495  dvnprodlem3  43496  voliooicof  43544  stoweidlem34  43582  stoweidlem42  43590  stoweidlem48  43596  dirkerf  43645  fourierdlem41  43696  fourierdlem51  43705  fourierdlem57  43711  fourierdlem60  43714  fourierdlem61  43715  fourierdlem73  43727  fourierdlem75  43729  fourierdlem103  43757  fourierdlem104  43758  etransclem1  43783  etransclem2  43784  etransclem20  43802  etransclem33  43815  etransclem46  43828  sge0isum  43972  sge0seq  43991  isomenndlem  44075  hoicvr  44093  ovnf  44108  ovnsubaddlem1  44115  hsphoif  44121  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnhoilem1  44146  ovnhoilem2  44147  ovncvr2  44156  hoidifhspf  44163  hspmbllem2  44172  iccvonmbllem  44223  vonioolem1  44225  vonioolem2  44226  vonicclem1  44228  vonicclem2  44229  fsetsniunop  44554  1hegrlfgr  45305  funcringcsetcALTV2lem3  45607  funcringcsetcALTV2lem9  45613  funcringcsetclem3ALTV  45630  funcringcsetclem9ALTV  45636  fdivmptf  45898  refdivmptf  45899  itcovalendof  46026  ackendofnn0  46041