Theorem feq1d 6670

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

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

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  feq1dd  6671  feq12d  6676  fco2  6714  fssres2  6728  fresin  6729  fresaun  6731  fmpt3d  7088  fressnfv  7132  f2ndf  8099  eroprf  8788  pmresg  8843  pw2f1olem  9045  ordtypelem4  9474  canthp1lem2  10606  fseq1p1m1  13559  repsf  14738  rlimres  15524  lo1res  15525  vdwapf  16943  fsets  17139  mrcf  17570  cofucl  17850  funcres  17858  funcestrcsetclem9  18109  1stfcl  18158  2ndfcl  18159  evlfcl  18183  yonedalem4c  18238  pmtrfinv  19391  pmtrff1o  19393  pmtrfcnv  19394  efgtf  19652  gsumzres  19839  isphld  21563  pjf  21622  frlmup1  21707  psrass1lem  21841  coe1f2  22094  lmbr  23145  tsmsres  24031  prdsdsf  24255  imasdsf1olem  24261  blfps  24294  blf  24295  tngngp2  24540  rrxmet  25308  ovolctb  25391  itg2monolem1  25651  itg2monolem2  25652  itg2monolem3  25653  itg2mono  25654  dvres  25812  dvres3a  25815  dvnff  25825  dvcmulf  25848  dvmptcl  25863  dvmptco  25876  dvlipcn  25899  dvgt0lem1  25907  itgsubstlem  25955  itgpowd  25957  dgrlem  26134  taylthlem1  26281  ulmval  26289  lgsfcl3  27229  midf  28703  grpodivf  30467  nvmf  30574  imsdf  30618  ipf  30642  0oo  30718  hoaddcl  31687  homulcl  31688  hosubcl  31702  fmptcof2  32581  ofoprabco  32588  fpwrelmap  32656  indf1ofs  32789  fedgmullem1  33625  sitmf  34343  fibp1  34392  ccatmulgnn0dir  34533  reprsuc  34606  pfxwlk  35111  cvmliftlem6  35277  cvmliftlem10  35281  mrsubff  35499  msubff  35517  tailf  36363  curf  37592  uncf  37593  poimirlem24  37638  ftc1anclem3  37689  rrnmet  37823  tendoplcl  40775  tendoicl  40790  intlewftc  42049  aks6d1c2  42118  aks6d1c6lem3  42160  pw2f1ocnv  43026  seff  44298  expgrowth  44324  dvnmul  45941  dvnprodlem2  45945  dvnprodlem3  45946  voliooicof  45994  stoweidlem34  46032  stoweidlem42  46040  stoweidlem48  46046  dirkerf  46095  fourierdlem41  46146  fourierdlem51  46155  fourierdlem57  46161  fourierdlem60  46164  fourierdlem61  46165  fourierdlem73  46177  fourierdlem75  46179  fourierdlem103  46207  fourierdlem104  46208  etransclem1  46233  etransclem2  46234  etransclem20  46252  etransclem33  46265  etransclem46  46278  sge0isum  46425  sge0seq  46444  isomenndlem  46528  hoicvr  46546  ovnf  46561  ovnsubaddlem1  46568  hsphoif  46574  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem1  46599  ovnhoilem2  46600  ovncvr2  46609  hoidifhspf  46616  hspmbllem2  46625  iccvonmbllem  46676  vonioolem1  46678  vonioolem2  46679  vonicclem1  46681  vonicclem2  46682  smfsupdmmbllem  46842  smfinfdmmbllem  46846  fsetsniunop  47050  1hegrlfgr  48120  funcringcsetcALTV2lem3  48280  funcringcsetcALTV2lem9  48286  funcringcsetclem3ALTV  48303  funcringcsetclem9ALTV  48309  fdivmptf  48530  refdivmptf  48531  itcovalendof  48658  ackendofnn0  48673  fucoppcid  49397  functermc  49497