Theorem feq1d 6530

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  ⟶wf 6376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-fun 6382  df-fn 6383  df-f 6384

This theorem is referenced by:  feq12d  6533  fco2  6572  fssres2  6587  fresin  6588  fresaun  6590  fmpt3d  6933  fressnfv  6975  f2ndf  7889  eroprf  8497  pmresg  8551  pw2f1olem  8749  ordtypelem4  9137  canthp1lem2  10267  fseq1p1m1  13186  repsf  14338  rlimres  15119  lo1res  15120  vdwapf  16525  fsets  16722  mrcf  17112  cofucl  17394  funcres  17402  funcestrcsetclem9  17655  1stfcl  17704  2ndfcl  17705  evlfcl  17730  yonedalem4c  17785  pmtrfinv  18853  pmtrff1o  18855  pmtrfcnv  18856  efgtf  19112  gsumzres  19294  isphld  20616  pjf  20675  frlmup1  20760  psrass1lemOLD  20899  psrass1lem  20902  coe1f2  21130  lmbr  22155  tsmsres  23041  prdsdsf  23265  imasdsf1olem  23271  blfps  23304  blf  23305  tngngp2  23550  rrxmet  24305  ovolctb  24387  itg2monolem1  24648  itg2monolem2  24649  itg2monolem3  24650  itg2mono  24651  dvres  24808  dvres3a  24811  dvnff  24820  dvcmulf  24842  dvmptcl  24856  dvmptco  24869  dvlipcn  24891  dvgt0lem1  24899  itgsubstlem  24945  itgpowd  24947  dgrlem  25123  taylthlem1  25265  ulmval  25272  lgsfcl3  26199  midf  26867  grpodivf  28619  nvmf  28726  imsdf  28770  ipf  28794  0oo  28870  hoaddcl  29839  homulcl  29840  hosubcl  29854  fmptcof2  30714  ofoprabco  30721  fpwrelmap  30788  fedgmullem1  31424  indf1ofs  31706  sitmf  32031  fibp1  32080  ccatmulgnn0dir  32233  reprsuc  32307  pfxwlk  32798  cvmliftlem6  32965  cvmliftlem10  32969  mrsubff  33187  msubff  33205  tailf  34301  curf  35492  uncf  35493  poimirlem24  35538  ftc1anclem3  35589  rrnmet  35724  tendoplcl  38532  tendoicl  38547  intlewftc  39803  pw2f1ocnv  40562  seff  41600  expgrowth  41626  feq1dd  42376  dvnmul  43159  dvnprodlem2  43163  dvnprodlem3  43164  voliooicof  43212  stoweidlem34  43250  stoweidlem42  43258  stoweidlem48  43264  dirkerf  43313  fourierdlem41  43364  fourierdlem51  43373  fourierdlem57  43379  fourierdlem60  43382  fourierdlem61  43383  fourierdlem73  43395  fourierdlem75  43397  fourierdlem103  43425  fourierdlem104  43426  etransclem1  43451  etransclem2  43452  etransclem20  43470  etransclem33  43483  etransclem46  43496  sge0isum  43640  sge0seq  43659  isomenndlem  43743  hoicvr  43761  ovnf  43776  ovnsubaddlem1  43783  hsphoif  43789  hoidmvlelem2  43809  hoidmvlelem3  43810  ovnhoilem1  43814  ovnhoilem2  43815  ovncvr2  43824  hoidifhspf  43831  hspmbllem2  43840  iccvonmbllem  43891  vonioolem1  43893  vonioolem2  43894  vonicclem1  43896  vonicclem2  43897  fsetsniunop  44215  1hegrlfgr  44967  funcringcsetcALTV2lem3  45269  funcringcsetcALTV2lem9  45275  funcringcsetclem3ALTV  45292  funcringcsetclem9ALTV  45298  fdivmptf  45560  refdivmptf  45561  itcovalendof  45688  ackendofnn0  45703