Theorem feq1i 6700

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 6687	. 2 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  ftpg  7160  fpropnf1  7271  suppsnop  8198  seqomlem2  8464  addnqf  11036  mulnqf  11037  isumsup2  16020  ruclem6  16408  sadcf  16628  sadadd2lem  16634  sadadd3  16636  sadaddlem  16641  smupf  16653  algrf  16753  funcoppc  18055  pmtr3ncomlem1  19692  znf1o  21862  ovolfsf  25797  ovolsf  25798  ovoliunlem1  25828  ovoliun  25831  ovoliun2  25832  voliunlem3  25878  itgss3  26140  dvexp  26278  plymul02  26606  efcn  26775  gamf  27375  basellem9  27421  axlowdimlem10  29534  wlkres  30254  1wlkdlem1  30733  vsfval  31240  ho0f  32358  opsqrlem4  32750  pjinvari  32798  fmptdf2  33297  mplmulmvr  34217  omssubaddlem  34977  omssubadd  34978  sitgclg  35020  sitgaddlemb  35026  coinfliprv  35161  signshf  35263  circum  36525  knoppcnlem8  37458  knoppcnlem11  37461  poimirlem31  38662  diophren  43913  clsf2  45219  seff  45386  binomcxplemnotnn0  45433  volicoff  47098  fourierdlem62  47271  fourierdlem80  47289  fourierdlem97  47306  carageniuncllem2  47625  0ome  47632  fcoresf1  48232  fcoresfo  48234  fundcmpsurinjimaid  48586  isubgruhgr  49059  lindslinindimp2lem2  49664  zlmodzxzldeplem1  49705  line2  49957