Theorem feq1i 6661

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

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

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 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  ftpg  7111  fpropnf1  7223  suppsnop  8130  seqomlem2  8392  addnqf  10871  mulnqf  10872  isumsup2  15781  ruclem6  16172  sadcf  16392  sadadd2lem  16398  sadadd3  16400  sadaddlem  16405  smupf  16417  algrf  16512  funcoppc  17811  pmtr3ncomlem1  19414  znf1o  21518  ovolfsf  25440  ovolsf  25441  ovoliunlem1  25471  ovoliun  25474  ovoliun2  25475  voliunlem3  25521  itgss3  25784  dvexp  25925  efcn  26421  gamf  27021  basellem9  27067  axlowdimlem10  29036  wlkres  29754  1wlkdlem1  30224  vsfval  30720  ho0f  31838  opsqrlem4  32230  pjinvari  32278  fmptdF  32745  mplmulmvr  33715  omssubaddlem  34476  omssubadd  34477  sitgclg  34519  sitgaddlemb  34525  coinfliprv  34660  plymul02  34723  signshf  34765  circum  35887  knoppcnlem8  36719  knoppcnlem11  36722  poimirlem31  37896  diophren  43164  clsf2  44476  seff  44659  binomcxplemnotnn0  44706  volicoff  46347  fourierdlem62  46520  fourierdlem80  46538  fourierdlem97  46555  carageniuncllem2  46874  0ome  46881  fcoresf1  47423  fcoresfo  47425  fundcmpsurinjimaid  47765  isubgruhgr  48222  lindslinindimp2lem2  48813  zlmodzxzldeplem1  48854  line2  49106