Theorem feq1d 6716

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-fun 6563  df-fn 6564  df-f 6565

This theorem is used by:  feq1dd  6717  feq12d  6722  fco2  6761  fssres2  6775  fresin  6776  fresaun  6778  fmpt3d  7143  fressnfv  7191  f2ndf  8161  eroprf  8867  curf  8921  uncf  8922  pmresg  8929  pw2f1olem  9131  ordtypelem4  9545  canthp1lem2  10768  fseq1p1m1  13762  repsf  14955  rlimres  15757  lo1res  15758  vdwapf  17182  fsets  17379  mrcf  17815  cofucl  18095  funcres  18103  funcestrcsetclem9  18354  1stfcl  18403  2ndfcl  18404  evlfcl  18428  yonedalem4c  18483  pmtrfinv  19708  pmtrff1o  19710  pmtrfcnv  19711  efgtf  19969  gsumzres  20156  isphld  21993  pjf  22052  frlmup1  22137  psrass1lem  22274  coe1f2  22560  lmbr  23609  tsmsres  24496  prdsdsf  24719  imasdsf1olem  24725  blfps  24758  blf  24759  tngngp2  25004  rrxmet  25762  ovolctb  25844  itg2monolem1  26104  itg2monolem2  26105  itg2monolem3  26106  itg2mono  26107  dvres  26264  dvres3a  26267  dvnff  26276  dvcmulf  26298  dvmptcl  26312  dvmptco  26325  dvlipcn  26347  dvgt0lem1  26355  itgsubstlem  26401  itgpowd  26403  dgrlem  26581  taylthlem1  26733  ulmval  26740  lgsfcl3  27678  midf  29314  pfxwlk  30299  grpodivf  31173  nvmf  31280  imsdf  31324  ipf  31348  0oo  31424  hoaddcl  32393  homulcl  32394  hosubcl  32408  fmptcof2  33326  ofoprabco  33333  fpwrelmap  33398  indf1ofs  33506  fedgmullem1  34344  sitmf  35067  fibp1  35116  ccatmulgnn0dir  35257  reprsuc  35327  cvmliftlem6  36235  cvmliftlem10  36239  mrsubff  36457  msubff  36475  tailf  37354  poimirlem24  38767  ftc1anclem3  38818  rrnmet  38966  tendoplcl  42041  tendoicl  42056  intlewftc  43314  aks6d1c2  43383  aks6d1c6lem3  43425  pw2f1ocnv  44248  seff  45496  expgrowth  45522  dvnmul  47168  dvnprodlem2  47172  dvnprodlem3  47173  voliooicof  47221  stoweidlem34  47259  stoweidlem42  47267  stoweidlem48  47273  dirkerf  47322  fourierdlem41  47373  fourierdlem51  47382  fourierdlem57  47388  fourierdlem60  47391  fourierdlem61  47392  fourierdlem73  47404  fourierdlem75  47406  fourierdlem103  47434  fourierdlem104  47435  etransclem1  47460  etransclem2  47461  etransclem20  47479  etransclem33  47492  etransclem46  47505  sge0isum  47652  sge0seq  47671  isomenndlem  47755  ovnf  47788  ovnsubaddlem1  47795  hsphoif  47801  hoidmvlelem2  47821  hoidmvlelem3  47822  ovnhoilem1  47826  ovnhoilem2  47827  ovncvr2  47836  hoidifhspf  47843  hspmbllem2  47852  iccvonmbllem  47903  vonioolem1  47905  vonioolem2  47906  vonicclem1  47908  vonicclem2  47909  smfsupdmmbllem  48069  smfinfdmmbllem  48073  fsetsniunop  48334  1hegrlfgr  49445  funcringcsetcALTV2lem3  49604  funcringcsetcALTV2lem9  49610  funcringcsetclem3ALTV  49627  funcringcsetclem9ALTV  49633  fdivmptf  49868  refdivmptf  49869  itcovalendof  49996  ackendofnn0  50011  fucoppcid  50758  functermc  50858