Theorem feq1i 6663

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

Syntax hints:   ↔ wb 206   = wceq 1542  ⟶wf 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-fun 6504  df-fn 6505  df-f 6506

This theorem is referenced by:  ftpg  7113  fpropnf1  7225  suppsnop  8132  seqomlem2  8394  addnqf  10873  mulnqf  10874  isumsup2  15783  ruclem6  16174  sadcf  16394  sadadd2lem  16400  sadadd3  16402  sadaddlem  16407  smupf  16419  algrf  16514  funcoppc  17813  pmtr3ncomlem1  19419  znf1o  21523  ovolfsf  25445  ovolsf  25446  ovoliunlem1  25476  ovoliun  25479  ovoliun2  25480  voliunlem3  25526  itgss3  25789  dvexp  25930  efcn  26426  gamf  27026  basellem9  27072  axlowdimlem10  29042  wlkres  29760  1wlkdlem1  30230  vsfval  30727  ho0f  31845  opsqrlem4  32237  pjinvari  32285  fmptdF  32752  mplmulmvr  33722  omssubaddlem  34483  omssubadd  34484  sitgclg  34526  sitgaddlemb  34532  coinfliprv  34667  plymul02  34730  signshf  34772  circum  35896  knoppcnlem8  36728  knoppcnlem11  36731  poimirlem31  37931  diophren  43199  clsf2  44511  seff  44694  binomcxplemnotnn0  44741  volicoff  46382  fourierdlem62  46555  fourierdlem80  46573  fourierdlem97  46590  carageniuncllem2  46909  0ome  46916  fcoresf1  47458  fcoresfo  47460  fundcmpsurinjimaid  47800  isubgruhgr  48257  lindslinindimp2lem2  48848  zlmodzxzldeplem1  48889  line2  49141