Theorem feq1d 6720

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-fun 6563  df-fn 6564  df-f 6565

This theorem is referenced by:  feq1dd  6721  feq12d  6724  fco2  6762  fssres2  6776  fresin  6777  fresaun  6779  fmpt3d  7136  fressnfv  7180  f2ndf  8145  eroprf  8855  pmresg  8910  pw2f1olem  9116  ordtypelem4  9561  canthp1lem2  10693  fseq1p1m1  13638  repsf  14811  rlimres  15594  lo1res  15595  vdwapf  17010  fsets  17206  mrcf  17652  cofucl  17933  funcres  17941  funcestrcsetclem9  18193  1stfcl  18242  2ndfcl  18243  evlfcl  18267  yonedalem4c  18322  pmtrfinv  19479  pmtrff1o  19481  pmtrfcnv  19482  efgtf  19740  gsumzres  19927  isphld  21672  pjf  21733  frlmup1  21818  psrass1lem  21952  coe1f2  22211  lmbr  23266  tsmsres  24152  prdsdsf  24377  imasdsf1olem  24383  blfps  24416  blf  24417  tngngp2  24673  rrxmet  25442  ovolctb  25525  itg2monolem1  25785  itg2monolem2  25786  itg2monolem3  25787  itg2mono  25788  dvres  25946  dvres3a  25949  dvnff  25959  dvcmulf  25982  dvmptcl  25997  dvmptco  26010  dvlipcn  26033  dvgt0lem1  26041  itgsubstlem  26089  itgpowd  26091  dgrlem  26268  taylthlem1  26415  ulmval  26423  lgsfcl3  27362  midf  28784  grpodivf  30557  nvmf  30664  imsdf  30708  ipf  30732  0oo  30808  hoaddcl  31777  homulcl  31778  hosubcl  31792  fmptcof2  32667  ofoprabco  32674  fpwrelmap  32744  indf1ofs  32851  fedgmullem1  33680  sitmf  34354  fibp1  34403  ccatmulgnn0dir  34557  reprsuc  34630  pfxwlk  35129  cvmliftlem6  35295  cvmliftlem10  35299  mrsubff  35517  msubff  35535  tailf  36376  curf  37605  uncf  37606  poimirlem24  37651  ftc1anclem3  37702  rrnmet  37836  tendoplcl  40783  tendoicl  40798  intlewftc  42062  aks6d1c2  42131  aks6d1c6lem3  42173  pw2f1ocnv  43049  seff  44328  expgrowth  44354  dvnmul  45958  dvnprodlem2  45962  dvnprodlem3  45963  voliooicof  46011  stoweidlem34  46049  stoweidlem42  46057  stoweidlem48  46063  dirkerf  46112  fourierdlem41  46163  fourierdlem51  46172  fourierdlem57  46178  fourierdlem60  46181  fourierdlem61  46182  fourierdlem73  46194  fourierdlem75  46196  fourierdlem103  46224  fourierdlem104  46225  etransclem1  46250  etransclem2  46251  etransclem20  46269  etransclem33  46282  etransclem46  46295  sge0isum  46442  sge0seq  46461  isomenndlem  46545  hoicvr  46563  ovnf  46578  ovnsubaddlem1  46585  hsphoif  46591  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoilem1  46616  ovnhoilem2  46617  ovncvr2  46626  hoidifhspf  46633  hspmbllem2  46642  iccvonmbllem  46693  vonioolem1  46695  vonioolem2  46696  vonicclem1  46698  vonicclem2  46699  smfsupdmmbllem  46859  smfinfdmmbllem  46863  fsetsniunop  47061  1hegrlfgr  48048  funcringcsetcALTV2lem3  48208  funcringcsetcALTV2lem9  48214  funcringcsetclem3ALTV  48231  funcringcsetclem9ALTV  48237  fdivmptf  48462  refdivmptf  48463  itcovalendof  48590  ackendofnn0  48605  functermc  49140