Theorem feq1d 6691

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  feq1dd  6692  feq12d  6697  fco2  6736  fssres2  6750  fresin  6751  fresaun  6753  fmpt3d  7116  fressnfv  7164  f2ndf  8133  eroprf  8839  curf  8893  uncf  8894  pmresg  8901  pw2f1olem  9103  ordtypelem4  9518  canthp1lem2  10741  fseq1p1m1  13735  repsf  14928  rlimres  15730  lo1res  15731  vdwapf  17155  fsets  17352  mrcf  17788  cofucl  18068  funcres  18076  funcestrcsetclem9  18327  1stfcl  18376  2ndfcl  18377  evlfcl  18401  yonedalem4c  18456  pmtrfinv  19680  pmtrff1o  19682  pmtrfcnv  19683  efgtf  19941  gsumzres  20128  isphld  21965  pjf  22024  frlmup1  22109  psrass1lem  22246  coe1f2  22532  lmbr  23581  tsmsres  24468  prdsdsf  24691  imasdsf1olem  24697  blfps  24730  blf  24731  tngngp2  24976  rrxmet  25734  ovolctb  25816  itg2monolem1  26076  itg2monolem2  26077  itg2monolem3  26078  itg2mono  26079  dvres  26236  dvres3a  26239  dvnff  26248  dvcmulf  26270  dvmptcl  26284  dvmptco  26297  dvlipcn  26319  dvgt0lem1  26327  itgsubstlem  26373  itgpowd  26375  dgrlem  26553  taylthlem1  26705  ulmval  26712  lgsfcl3  27650  midf  29286  pfxwlk  30271  grpodivf  31145  nvmf  31252  imsdf  31296  ipf  31320  0oo  31396  hoaddcl  32365  homulcl  32366  hosubcl  32380  fmptcof2  33298  ofoprabco  33305  fpwrelmap  33371  indf1ofs  33479  fedgmullem1  34307  sitmf  35030  fibp1  35079  ccatmulgnn0dir  35220  reprsuc  35290  cvmliftlem6  36141  cvmliftlem10  36145  mrsubff  36363  msubff  36381  tailf  37255  poimirlem24  38655  ftc1anclem3  38706  rrnmet  38856  tendoplcl  41931  tendoicl  41946  intlewftc  43204  aks6d1c2  43273  aks6d1c6lem3  43315  pw2f1ocnv  44137  seff  45386  expgrowth  45412  dvnmul  47046  dvnprodlem2  47050  dvnprodlem3  47051  voliooicof  47099  stoweidlem34  47137  stoweidlem42  47145  stoweidlem48  47151  dirkerf  47200  fourierdlem41  47251  fourierdlem51  47260  fourierdlem57  47266  fourierdlem60  47269  fourierdlem61  47270  fourierdlem73  47282  fourierdlem75  47284  fourierdlem103  47312  fourierdlem104  47313  etransclem1  47338  etransclem2  47339  etransclem20  47357  etransclem33  47370  etransclem46  47383  sge0isum  47530  sge0seq  47549  isomenndlem  47633  ovnf  47666  ovnsubaddlem1  47673  hsphoif  47679  hoidmvlelem2  47699  hoidmvlelem3  47700  ovnhoilem1  47704  ovnhoilem2  47705  ovncvr2  47714  hoidifhspf  47721  hspmbllem2  47730  iccvonmbllem  47781  vonioolem1  47783  vonioolem2  47784  vonicclem1  47786  vonicclem2  47787  smfsupdmmbllem  47947  smfinfdmmbllem  47951  fsetsniunop  48212  1hegrlfgr  49323  funcringcsetcALTV2lem3  49482  funcringcsetcALTV2lem9  49488  funcringcsetclem3ALTV  49505  funcringcsetclem9ALTV  49511  fdivmptf  49746  refdivmptf  49747  itcovalendof  49874  ackendofnn0  49889  fucoppcid  50636  functermc  50736