Theorem feq1d 6634

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-fun 6484  df-fn 6485  df-f 6486

This theorem is referenced by:  feq1dd  6635  feq12d  6640  fco2  6678  fssres2  6692  fresin  6693  fresaun  6695  fmpt3d  7050  fressnfv  7094  f2ndf  8053  eroprf  8742  pmresg  8797  pw2f1olem  8998  ordtypelem4  9413  canthp1lem2  10547  fseq1p1m1  13501  repsf  14679  rlimres  15465  lo1res  15466  vdwapf  16884  fsets  17080  mrcf  17515  cofucl  17795  funcres  17803  funcestrcsetclem9  18054  1stfcl  18103  2ndfcl  18104  evlfcl  18128  yonedalem4c  18183  pmtrfinv  19340  pmtrff1o  19342  pmtrfcnv  19343  efgtf  19601  gsumzres  19788  isphld  21561  pjf  21620  frlmup1  21705  psrass1lem  21839  coe1f2  22092  lmbr  23143  tsmsres  24029  prdsdsf  24253  imasdsf1olem  24259  blfps  24292  blf  24293  tngngp2  24538  rrxmet  25306  ovolctb  25389  itg2monolem1  25649  itg2monolem2  25650  itg2monolem3  25651  itg2mono  25652  dvres  25810  dvres3a  25813  dvnff  25823  dvcmulf  25846  dvmptcl  25861  dvmptco  25874  dvlipcn  25897  dvgt0lem1  25905  itgsubstlem  25953  itgpowd  25955  dgrlem  26132  taylthlem1  26279  ulmval  26287  lgsfcl3  27227  midf  28725  grpodivf  30486  nvmf  30593  imsdf  30637  ipf  30661  0oo  30737  hoaddcl  31706  homulcl  31707  hosubcl  31721  fmptcof2  32608  ofoprabco  32615  fpwrelmap  32685  indf1ofs  32818  fedgmullem1  33612  sitmf  34336  fibp1  34385  ccatmulgnn0dir  34526  reprsuc  34599  pfxwlk  35117  cvmliftlem6  35283  cvmliftlem10  35287  mrsubff  35505  msubff  35523  tailf  36369  curf  37598  uncf  37599  poimirlem24  37644  ftc1anclem3  37695  rrnmet  37829  tendoplcl  40780  tendoicl  40795  intlewftc  42054  aks6d1c2  42123  aks6d1c6lem3  42165  pw2f1ocnv  43030  seff  44302  expgrowth  44328  dvnmul  45944  dvnprodlem2  45948  dvnprodlem3  45949  voliooicof  45997  stoweidlem34  46035  stoweidlem42  46043  stoweidlem48  46049  dirkerf  46098  fourierdlem41  46149  fourierdlem51  46158  fourierdlem57  46164  fourierdlem60  46167  fourierdlem61  46168  fourierdlem73  46180  fourierdlem75  46182  fourierdlem103  46210  fourierdlem104  46211  etransclem1  46236  etransclem2  46237  etransclem20  46255  etransclem33  46268  etransclem46  46281  sge0isum  46428  sge0seq  46447  isomenndlem  46531  hoicvr  46549  ovnf  46564  ovnsubaddlem1  46571  hsphoif  46577  hoidmvlelem2  46597  hoidmvlelem3  46598  ovnhoilem1  46602  ovnhoilem2  46603  ovncvr2  46612  hoidifhspf  46619  hspmbllem2  46628  iccvonmbllem  46679  vonioolem1  46681  vonioolem2  46682  vonicclem1  46684  vonicclem2  46685  smfsupdmmbllem  46845  smfinfdmmbllem  46849  fsetsniunop  47053  1hegrlfgr  48136  funcringcsetcALTV2lem3  48296  funcringcsetcALTV2lem9  48302  funcringcsetclem3ALTV  48319  funcringcsetclem9ALTV  48325  fdivmptf  48546  refdivmptf  48547  itcovalendof  48674  ackendofnn0  48689  fucoppcid  49413  functermc  49513