Theorem feq1i 5949

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

Syntax hints:   ↔ wb 195   = wceq 1475  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-fun 5806  df-fn 5807  df-f 5808

This theorem is referenced by:  ftpg  6328  suppsnop  7196  seqomlem2  7433  addnqf  9649  mulnqf  9650  hashfOLD  12988  isumsup2  14417  ruclem6  14803  sadcf  15013  sadadd2lem  15019  sadadd3  15021  sadaddlem  15026  smupf  15038  algrf  15124  funcoppc  16358  pmtr3ncomlem1  17716  znf1o  19719  ovolfsf  23047  ovolsf  23048  ovoliunlem1  23077  ovoliun  23080  ovoliun2  23081  voliunlem3  23127  itgss3  23387  dvexp  23522  efcn  24001  gamf  24569  basellem9  24615  axlowdimlem10  25631  uhgrares  25837  umgrares  25853  2trllemH  26082  2trllemG  26088  wlkntrllem1  26089  wlkntrllem3  26091  eupares  26502  vsfval  26872  ho0f  27994  opsqrlem4  28386  pjinvari  28434  fmptdF  28836  omssubaddlem  29688  omssubadd  29689  sitgclg  29731  sitgaddlemb  29737  coinfliprv  29871  plymul02  29949  signshf  29991  circum  30822  knoppcnlem8  31660  knoppcnlem11  31663  poimirlem31  32610  diophren  36395  clsf2  37444  seff  37530  binomcxplemnotnn0  37577  volicoff  38888  fourierdlem62  39061  fourierdlem80  39079  fourierdlem97  39096  carageniuncllem2  39412  0ome  39419  fpropnf1  40337  1wlkres  40879  11wlkdlem1  41304  mapprop  41917  lindslinindimp2lem2  42042  zlmodzxzldeplem1  42083