Theorem feq1i 6703

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

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

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  ftpg  7160  fpropnf1  7272  suppsnop  8183  seqomlem2  8447  addnqf  10951  mulnqf  10952  isumsup2  15926  ruclem6  16316  sadcf  16536  sadadd2lem  16542  sadadd3  16544  sadaddlem  16549  smupf  16561  algrf  16656  funcoppc  17957  pmtr3ncomlem1  19574  znf1o  21738  ovolfsf  25667  ovolsf  25668  ovoliunlem1  25698  ovoliun  25701  ovoliun2  25702  voliunlem3  25748  itgss3  26011  dvexp  26149  plymul02  26478  efcn  26643  gamf  27244  basellem9  27290  axlowdimlem10  29338  wlkres  30055  1wlkdlem1  30525  vsfval  31022  ho0f  32140  opsqrlem4  32532  pjinvari  32580  fmptdf2  33038  mplmulmvr  33960  omssubaddlem  34721  omssubadd  34722  sitgclg  34764  sitgaddlemb  34770  coinfliprv  34905  signshf  35007  circum  36187  knoppcnlem8  37130  knoppcnlem11  37133  poimirlem31  38343  diophren  43581  clsf2  44893  seff  45060  binomcxplemnotnn0  45107  volicoff  46750  fourierdlem62  46923  fourierdlem80  46941  fourierdlem97  46958  carageniuncllem2  47277  0ome  47284  fcoresf1  47847  fcoresfo  47849  fundcmpsurinjimaid  48201  isubgruhgr  48674  lindslinindimp2lem2  49280  zlmodzxzldeplem1  49321  line2  49573