Theorem feq1d 6690

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-fun 6533  df-fn 6534  df-f 6535

This theorem is referenced by:  feq1dd  6691  feq12d  6694  fco2  6732  fssres2  6746  fresin  6747  fresaun  6749  fmpt3d  7106  fressnfv  7150  f2ndf  8119  eroprf  8829  pmresg  8884  pw2f1olem  9090  ordtypelem4  9535  canthp1lem2  10667  fseq1p1m1  13615  repsf  14791  rlimres  15574  lo1res  15575  vdwapf  16992  fsets  17188  mrcf  17621  cofucl  17901  funcres  17909  funcestrcsetclem9  18160  1stfcl  18209  2ndfcl  18210  evlfcl  18234  yonedalem4c  18289  pmtrfinv  19442  pmtrff1o  19444  pmtrfcnv  19445  efgtf  19703  gsumzres  19890  isphld  21614  pjf  21673  frlmup1  21758  psrass1lem  21892  coe1f2  22145  lmbr  23196  tsmsres  24082  prdsdsf  24306  imasdsf1olem  24312  blfps  24345  blf  24346  tngngp2  24591  rrxmet  25360  ovolctb  25443  itg2monolem1  25703  itg2monolem2  25704  itg2monolem3  25705  itg2mono  25706  dvres  25864  dvres3a  25867  dvnff  25877  dvcmulf  25900  dvmptcl  25915  dvmptco  25928  dvlipcn  25951  dvgt0lem1  25959  itgsubstlem  26007  itgpowd  26009  dgrlem  26186  taylthlem1  26333  ulmval  26341  lgsfcl3  27281  midf  28755  grpodivf  30519  nvmf  30626  imsdf  30670  ipf  30694  0oo  30770  hoaddcl  31739  homulcl  31740  hosubcl  31754  fmptcof2  32635  ofoprabco  32642  fpwrelmap  32710  indf1ofs  32843  fedgmullem1  33669  sitmf  34384  fibp1  34433  ccatmulgnn0dir  34574  reprsuc  34647  pfxwlk  35146  cvmliftlem6  35312  cvmliftlem10  35316  mrsubff  35534  msubff  35552  tailf  36393  curf  37622  uncf  37623  poimirlem24  37668  ftc1anclem3  37719  rrnmet  37853  tendoplcl  40800  tendoicl  40815  intlewftc  42074  aks6d1c2  42143  aks6d1c6lem3  42185  pw2f1ocnv  43061  seff  44333  expgrowth  44359  dvnmul  45972  dvnprodlem2  45976  dvnprodlem3  45977  voliooicof  46025  stoweidlem34  46063  stoweidlem42  46071  stoweidlem48  46077  dirkerf  46126  fourierdlem41  46177  fourierdlem51  46186  fourierdlem57  46192  fourierdlem60  46195  fourierdlem61  46196  fourierdlem73  46208  fourierdlem75  46210  fourierdlem103  46238  fourierdlem104  46239  etransclem1  46264  etransclem2  46265  etransclem20  46283  etransclem33  46296  etransclem46  46309  sge0isum  46456  sge0seq  46475  isomenndlem  46559  hoicvr  46577  ovnf  46592  ovnsubaddlem1  46599  hsphoif  46605  hoidmvlelem2  46625  hoidmvlelem3  46626  ovnhoilem1  46630  ovnhoilem2  46631  ovncvr2  46640  hoidifhspf  46647  hspmbllem2  46656  iccvonmbllem  46707  vonioolem1  46709  vonioolem2  46710  vonicclem1  46712  vonicclem2  46713  smfsupdmmbllem  46873  smfinfdmmbllem  46877  fsetsniunop  47078  1hegrlfgr  48107  funcringcsetcALTV2lem3  48267  funcringcsetcALTV2lem9  48273  funcringcsetclem3ALTV  48290  funcringcsetclem9ALTV  48296  fdivmptf  48521  refdivmptf  48522  itcovalendof  48649  ackendofnn0  48664  functermc  49393