Theorem feq1d 6688

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  feq1dd  6689  feq12d  6694  fco2  6733  fssres2  6747  fresin  6748  fresaun  6750  fmpt3d  7113  fressnfv  7161  f2ndf  8121  eroprf  8819  curf  8873  uncf  8874  pmresg  8881  pw2f1olem  9083  ordtypelem4  9497  canthp1lem2  10666  fseq1p1m1  13657  repsf  14848  rlimres  15649  lo1res  15650  vdwapf  17070  fsets  17267  mrcf  17703  cofucl  17983  funcres  17991  funcestrcsetclem9  18242  1stfcl  18291  2ndfcl  18292  evlfcl  18316  yonedalem4c  18371  pmtrfinv  19594  pmtrff1o  19596  pmtrfcnv  19597  efgtf  19855  gsumzres  20042  isphld  21873  pjf  21932  frlmup1  22017  psrass1lem  22154  coe1f2  22440  lmbr  23489  tsmsres  24376  prdsdsf  24599  imasdsf1olem  24605  blfps  24638  blf  24639  tngngp2  24884  rrxmet  25642  ovolctb  25724  itg2monolem1  25984  itg2monolem2  25985  itg2monolem3  25986  itg2mono  25987  dvres  26145  dvres3a  26148  dvnff  26157  dvcmulf  26179  dvmptcl  26193  dvmptco  26206  dvlipcn  26228  dvgt0lem1  26236  itgsubstlem  26282  itgpowd  26284  dgrlem  26462  taylthlem1  26616  ulmval  26623  lgsfcl3  27562  midf  29168  pfxwlk  30153  grpodivf  31027  nvmf  31134  imsdf  31178  ipf  31202  0oo  31278  hoaddcl  32247  homulcl  32248  hosubcl  32262  fmptcof2  33138  ofoprabco  33145  fpwrelmap  33212  indf1ofs  33320  fedgmullem1  34147  sitmf  34871  fibp1  34920  ccatmulgnn0dir  35061  reprsuc  35131  cvmliftlem6  35877  cvmliftlem10  35881  mrsubff  36099  msubff  36117  tailf  37002  poimirlem24  38401  ftc1anclem3  38452  rrnmet  38587  tendoplcl  41662  tendoicl  41677  intlewftc  42935  aks6d1c2  43004  aks6d1c6lem3  43046  pw2f1ocnv  43886  seff  45141  expgrowth  45167  dvnmul  46779  dvnprodlem2  46783  dvnprodlem3  46784  voliooicof  46832  stoweidlem34  46870  stoweidlem42  46878  stoweidlem48  46884  dirkerf  46933  fourierdlem41  46984  fourierdlem51  46993  fourierdlem57  46999  fourierdlem60  47002  fourierdlem61  47003  fourierdlem73  47015  fourierdlem75  47017  fourierdlem103  47045  fourierdlem104  47046  etransclem1  47071  etransclem2  47072  etransclem20  47090  etransclem33  47103  etransclem46  47116  sge0isum  47263  sge0seq  47282  isomenndlem  47366  ovnf  47399  ovnsubaddlem1  47406  hsphoif  47412  hoidmvlelem2  47432  hoidmvlelem3  47433  ovnhoilem1  47437  ovnhoilem2  47438  ovncvr2  47447  hoidifhspf  47454  hspmbllem2  47463  iccvonmbllem  47514  vonioolem1  47516  vonioolem2  47517  vonicclem1  47519  vonicclem2  47520  smfsupdmmbllem  47680  smfinfdmmbllem  47684  fsetsniunop  47945  1hegrlfgr  49056  funcringcsetcALTV2lem3  49215  funcringcsetcALTV2lem9  49221  funcringcsetclem3ALTV  49238  funcringcsetclem9ALTV  49244  fdivmptf  49479  refdivmptf  49480  itcovalendof  49607  ackendofnn0  49622  fucoppcid  50342  functermc  50442