Theorem feq1i 6692

Description: Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
feq1i.1	⊢ 𝐹 = 𝐺

Assertion

Ref	Expression
feq1i	⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)

Proof of Theorem feq1i

Step	Hyp	Ref	Expression
1		feq1i.1	. 2 ⊢ 𝐹 = 𝐺
2		feq1 6679	. 2 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ⟶wf 6527

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6533  df-fn 6534  df-f 6535

This theorem is used by:  ftpg  7152  fpropnf1  7263  suppsnop  8179  seqomlem2  8445  addnqf  11014  mulnqf  11015  isumsup2  15995  ruclem6  16383  sadcf  16603  sadadd2lem  16609  sadadd3  16611  sadaddlem  16616  smupf  16628  algrf  16728  funcoppc  18030  pmtr3ncomlem1  19667  znf1o  21837  ovolfsf  25772  ovolsf  25773  ovoliunlem1  25803  ovoliun  25806  ovoliun2  25807  voliunlem3  25853  itgss3  26115  dvexp  26253  plymul02  26583  efcn  26752  gamf  27352  basellem9  27398  axlowdimlem10  29511  wlkres  30231  1wlkdlem1  30710  vsfval  31217  ho0f  32335  opsqrlem4  32727  pjinvari  32775  fmptdf2  33232  mplmulmvr  34153  omssubaddlem  34914  omssubadd  34915  sitgclg  34957  sitgaddlemb  34963  coinfliprv  35098  signshf  35200  circum  36408  knoppcnlem8  37336  knoppcnlem11  37339  poimirlem31  38537  diophren  43773  clsf2  45085  seff  45252  binomcxplemnotnn0  45299  volicoff  46949  fourierdlem62  47122  fourierdlem80  47140  fourierdlem97  47157  carageniuncllem2  47476  0ome  47483  fcoresf1  48083  fcoresfo  48085  fundcmpsurinjimaid  48437  isubgruhgr  48910  lindslinindimp2lem2  49515  zlmodzxzldeplem1  49556  line2  49808