Theorem feq1i 6653

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

Syntax hints:   ↔ wb 206   = wceq 1541  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  ftpg  7101  fpropnf1  7213  suppsnop  8120  seqomlem2  8382  addnqf  10859  mulnqf  10860  isumsup2  15769  ruclem6  16160  sadcf  16380  sadadd2lem  16386  sadadd3  16388  sadaddlem  16393  smupf  16405  algrf  16500  funcoppc  17799  pmtr3ncomlem1  19402  znf1o  21506  ovolfsf  25428  ovolsf  25429  ovoliunlem1  25459  ovoliun  25462  ovoliun2  25463  voliunlem3  25509  itgss3  25772  dvexp  25913  efcn  26409  gamf  27009  basellem9  27055  axlowdimlem10  29024  wlkres  29742  1wlkdlem1  30212  vsfval  30708  ho0f  31826  opsqrlem4  32218  pjinvari  32266  fmptdF  32734  mplmulmvr  33704  omssubaddlem  34456  omssubadd  34457  sitgclg  34499  sitgaddlemb  34505  coinfliprv  34640  plymul02  34703  signshf  34745  circum  35868  knoppcnlem8  36700  knoppcnlem11  36703  poimirlem31  37848  diophren  43051  clsf2  44363  seff  44546  binomcxplemnotnn0  44593  volicoff  46235  fourierdlem62  46408  fourierdlem80  46426  fourierdlem97  46443  carageniuncllem2  46762  0ome  46769  fcoresf1  47311  fcoresfo  47313  fundcmpsurinjimaid  47653  isubgruhgr  48110  lindslinindimp2lem2  48701  zlmodzxzldeplem1  48742  line2  48994