Theorem feq1d 6359

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1520  ⟶wf 6213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-br 4957  df-opab 5019  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-fun 6219  df-fn 6220  df-f 6221

This theorem is referenced by:  feq12d  6362  fco2  6393  fssres2  6406  fresin  6407  fresaun  6409  fmpt3d  6734  fressnfv  6776  f2ndf  7660  eroprf  8236  pmresg  8275  pw2f1olem  8458  ordtypelem4  8821  canthp1lem2  9910  fseq1p1m1  12820  repsf  13959  rlimres  14737  lo1res  14738  vdwapf  16125  fsets  16333  mrcf  16697  cofucl  16975  funcres  16983  funcestrcsetclem9  17215  1stfcl  17264  2ndfcl  17265  evlfcl  17289  yonedalem4c  17344  pmtrfinv  18308  pmtrff1o  18310  pmtrfcnv  18311  efgtf  18563  gsumzres  18738  psrass1lem  19833  coe1f2  20048  isphld  20468  pjf  20527  frlmup1  20612  lmbr  21538  tsmsres  22423  prdsdsf  22648  imasdsf1olem  22654  blfps  22687  blf  22688  tngngp2  22932  rrxmet  23682  ovolctb  23762  itg2monolem1  24022  itg2monolem2  24023  itg2monolem3  24024  itg2mono  24025  dvres  24180  dvres3a  24183  dvnff  24191  dvcmulf  24213  dvmptcl  24227  dvmptco  24240  dvlipcn  24262  dvgt0lem1  24270  itgsubstlem  24316  dgrlem  24490  taylthlem1  24632  ulmval  24639  lgsfcl3  25564  midf  26232  grpodivf  27994  nvmf  28101  imsdf  28145  ipf  28169  0oo  28245  hoaddcl  29214  homulcl  29215  hosubcl  29229  fmptcof2  30065  ofoprabco  30072  fpwrelmap  30130  fedgmullem1  30584  indf1ofs  30858  sitmf  31183  fibp1  31232  ccatmulgnn0dir  31385  reprsuc  31459  cvmliftlem6  32101  cvmliftlem10  32105  mrsubff  32312  msubff  32330  tailf  33277  curf  34347  uncf  34348  poimirlem24  34393  ftc1anclem3  34446  rrnmet  34585  tendoplcl  37398  tendoicl  37413  pw2f1ocnv  39070  itgpowd  39257  seff  40131  expgrowth  40157  feq1dd  40916  dvnmul  41723  dvnprodlem2  41727  dvnprodlem3  41728  voliooicof  41777  stoweidlem34  41815  stoweidlem42  41823  stoweidlem48  41829  dirkerf  41878  fourierdlem41  41929  fourierdlem51  41938  fourierdlem57  41944  fourierdlem60  41947  fourierdlem61  41948  fourierdlem73  41960  fourierdlem75  41962  fourierdlem103  41990  fourierdlem104  41991  etransclem1  42016  etransclem2  42017  etransclem20  42035  etransclem33  42048  etransclem46  42061  sge0isum  42205  sge0seq  42224  isomenndlem  42308  hoicvr  42326  ovnf  42341  ovnsubaddlem1  42348  hsphoif  42354  hoidmvlelem2  42374  hoidmvlelem3  42375  ovnhoilem1  42379  ovnhoilem2  42380  ovncvr2  42389  hoidifhspf  42396  hspmbllem2  42405  iccvonmbllem  42456  vonioolem1  42458  vonioolem2  42459  vonicclem1  42461  vonicclem2  42462  1hegrlfgr  43443  funcringcsetcALTV2lem3  43741  funcringcsetcALTV2lem9  43747  funcringcsetclem3ALTV  43764  funcringcsetclem9ALTV  43770  fdivmptf  44036  refdivmptf  44037