Theorem feq1i 6697

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  ftpg  7157  fpropnf1  7268  suppsnop  8180  seqomlem2  8444  addnqf  10961  mulnqf  10962  isumsup2  15939  ruclem6  16329  sadcf  16549  sadadd2lem  16555  sadadd3  16557  sadaddlem  16562  smupf  16574  algrf  16669  funcoppc  17970  pmtr3ncomlem1  19606  znf1o  21770  ovolfsf  25705  ovolsf  25706  ovoliunlem1  25736  ovoliun  25739  ovoliun2  25740  voliunlem3  25786  itgss3  26049  dvexp  26187  plymul02  26517  efcn  26686  gamf  27287  basellem9  27333  axlowdimlem10  29416  wlkres  30136  1wlkdlem1  30615  vsfval  31122  ho0f  32240  opsqrlem4  32632  pjinvari  32680  fmptdf2  33137  mplmulmvr  34057  omssubaddlem  34818  omssubadd  34819  sitgclg  34861  sitgaddlemb  34867  coinfliprv  35002  signshf  35104  circum  36261  knoppcnlem8  37205  knoppcnlem11  37208  poimirlem31  38408  diophren  43662  clsf2  44974  seff  45141  binomcxplemnotnn0  45188  volicoff  46831  fourierdlem62  47004  fourierdlem80  47022  fourierdlem97  47039  carageniuncllem2  47358  0ome  47365  fcoresf1  47965  fcoresfo  47967  fundcmpsurinjimaid  48319  isubgruhgr  48792  lindslinindimp2lem2  49397  zlmodzxzldeplem1  49438  line2  49690