Theorem feq1d 6673

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  feq1dd  6674  feq12d  6679  fco2  6717  fssres2  6731  fresin  6732  fresaun  6734  fmpt3d  7091  fressnfv  7135  f2ndf  8102  eroprf  8791  pmresg  8846  pw2f1olem  9050  ordtypelem4  9481  canthp1lem2  10613  fseq1p1m1  13566  repsf  14745  rlimres  15531  lo1res  15532  vdwapf  16950  fsets  17146  mrcf  17577  cofucl  17857  funcres  17865  funcestrcsetclem9  18116  1stfcl  18165  2ndfcl  18166  evlfcl  18190  yonedalem4c  18245  pmtrfinv  19398  pmtrff1o  19400  pmtrfcnv  19401  efgtf  19659  gsumzres  19846  isphld  21570  pjf  21629  frlmup1  21714  psrass1lem  21848  coe1f2  22101  lmbr  23152  tsmsres  24038  prdsdsf  24262  imasdsf1olem  24268  blfps  24301  blf  24302  tngngp2  24547  rrxmet  25315  ovolctb  25398  itg2monolem1  25658  itg2monolem2  25659  itg2monolem3  25660  itg2mono  25661  dvres  25819  dvres3a  25822  dvnff  25832  dvcmulf  25855  dvmptcl  25870  dvmptco  25883  dvlipcn  25906  dvgt0lem1  25914  itgsubstlem  25962  itgpowd  25964  dgrlem  26141  taylthlem1  26288  ulmval  26296  lgsfcl3  27236  midf  28710  grpodivf  30474  nvmf  30581  imsdf  30625  ipf  30649  0oo  30725  hoaddcl  31694  homulcl  31695  hosubcl  31709  fmptcof2  32588  ofoprabco  32595  fpwrelmap  32663  indf1ofs  32796  fedgmullem1  33632  sitmf  34350  fibp1  34399  ccatmulgnn0dir  34540  reprsuc  34613  pfxwlk  35118  cvmliftlem6  35284  cvmliftlem10  35288  mrsubff  35506  msubff  35524  tailf  36370  curf  37599  uncf  37600  poimirlem24  37645  ftc1anclem3  37696  rrnmet  37830  tendoplcl  40782  tendoicl  40797  intlewftc  42056  aks6d1c2  42125  aks6d1c6lem3  42167  pw2f1ocnv  43033  seff  44305  expgrowth  44331  dvnmul  45948  dvnprodlem2  45952  dvnprodlem3  45953  voliooicof  46001  stoweidlem34  46039  stoweidlem42  46047  stoweidlem48  46053  dirkerf  46102  fourierdlem41  46153  fourierdlem51  46162  fourierdlem57  46168  fourierdlem60  46171  fourierdlem61  46172  fourierdlem73  46184  fourierdlem75  46186  fourierdlem103  46214  fourierdlem104  46215  etransclem1  46240  etransclem2  46241  etransclem20  46259  etransclem33  46272  etransclem46  46285  sge0isum  46432  sge0seq  46451  isomenndlem  46535  hoicvr  46553  ovnf  46568  ovnsubaddlem1  46575  hsphoif  46581  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnhoilem1  46606  ovnhoilem2  46607  ovncvr2  46616  hoidifhspf  46623  hspmbllem2  46632  iccvonmbllem  46683  vonioolem1  46685  vonioolem2  46686  vonicclem1  46688  vonicclem2  46689  smfsupdmmbllem  46849  smfinfdmmbllem  46853  fsetsniunop  47054  1hegrlfgr  48124  funcringcsetcALTV2lem3  48284  funcringcsetcALTV2lem9  48290  funcringcsetclem3ALTV  48307  funcringcsetclem9ALTV  48313  fdivmptf  48534  refdivmptf  48535  itcovalendof  48662  ackendofnn0  48677  fucoppcid  49401  functermc  49501