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 207   = wceq 1547  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  ftpg  7106  fpropnf1  7218  suppsnop  8125  seqomlem2  8387  addnqf  10869  mulnqf  10870  isumsup2  15809  ruclem6  16200  sadcf  16420  sadadd2lem  16426  sadadd3  16428  sadaddlem  16433  smupf  16445  algrf  16540  funcoppc  17840  pmtr3ncomlem1  19446  znf1o  21533  ovolfsf  25463  ovolsf  25464  ovoliunlem1  25494  ovoliun  25497  ovoliun2  25498  voliunlem3  25544  itgss3  25807  dvexp  25945  efcn  26433  gamf  27031  basellem9  27077  axlowdimlem10  29045  wlkres  29762  1wlkdlem1  30232  vsfval  30729  ho0f  31847  opsqrlem4  32239  pjinvari  32287  fmptdF  32755  mplmulmvr  33730  omssubaddlem  34490  omssubadd  34491  sitgclg  34533  sitgaddlemb  34539  coinfliprv  34674  plymul02  34737  signshf  34779  circum  35909  knoppcnlem8  36813  knoppcnlem11  36816  poimirlem31  38025  diophren  43265  clsf2  44577  seff  44760  binomcxplemnotnn0  44807  volicoff  46445  fourierdlem62  46618  fourierdlem80  46636  fourierdlem97  46653  carageniuncllem2  46972  0ome  46979  fcoresf1  47539  fcoresfo  47541  fundcmpsurinjimaid  47893  isubgruhgr  48366  lindslinindimp2lem2  48957  zlmodzxzldeplem1  48998  line2  49250