Theorem feq1i 6197

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

Syntax hints:   ↔ wb 196   = wceq 1632  ⟶wf 6045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-fun 6051  df-fn 6052  df-f 6053

This theorem is referenced by:  ftpg  6586  fpropnf1  6687  suppsnop  7477  seqomlem2  7715  addnqf  9962  mulnqf  9963  hashfOLD  13320  isumsup2  14777  ruclem6  15163  sadcf  15377  sadadd2lem  15383  sadadd3  15385  sadaddlem  15390  smupf  15402  algrf  15488  funcoppc  16736  pmtr3ncomlem1  18093  znf1o  20102  ovolfsf  23440  ovolsf  23441  ovoliunlem1  23470  ovoliun  23473  ovoliun2  23474  voliunlem3  23520  itgss3  23780  dvexp  23915  efcn  24396  gamf  24968  basellem9  25014  axlowdimlem10  26030  wlkres  26777  1wlkdlem1  27289  vsfval  27797  ho0f  28919  opsqrlem4  29311  pjinvari  29359  fmptdF  29765  omssubaddlem  30670  omssubadd  30671  sitgclg  30713  sitgaddlemb  30719  coinfliprv  30853  plymul02  30932  signshf  30974  circum  31875  knoppcnlem8  32796  knoppcnlem11  32799  poimirlem31  33753  diophren  37879  clsf2  38926  seff  39010  binomcxplemnotnn0  39057  volicoff  40715  fourierdlem62  40888  fourierdlem80  40906  fourierdlem97  40923  carageniuncllem2  41242  0ome  41249  mapprop  42634  lindslinindimp2lem2  42758  zlmodzxzldeplem1  42799