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 206   = wceq 1542  ⟶wf 6488

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  ftpg  7103  fpropnf1  7215  suppsnop  8121  seqomlem2  8383  addnqf  10862  mulnqf  10863  isumsup2  15802  ruclem6  16193  sadcf  16413  sadadd2lem  16419  sadadd3  16421  sadaddlem  16426  smupf  16438  algrf  16533  funcoppc  17833  pmtr3ncomlem1  19439  znf1o  21541  ovolfsf  25448  ovolsf  25449  ovoliunlem1  25479  ovoliun  25482  ovoliun2  25483  voliunlem3  25529  itgss3  25792  dvexp  25930  efcn  26421  gamf  27020  basellem9  27066  axlowdimlem10  29034  wlkres  29752  1wlkdlem1  30222  vsfval  30719  ho0f  31837  opsqrlem4  32229  pjinvari  32277  fmptdF  32744  mplmulmvr  33698  omssubaddlem  34459  omssubadd  34460  sitgclg  34502  sitgaddlemb  34508  coinfliprv  34643  plymul02  34706  signshf  34748  circum  35872  knoppcnlem8  36776  knoppcnlem11  36779  poimirlem31  37986  diophren  43259  clsf2  44571  seff  44754  binomcxplemnotnn0  44801  volicoff  46441  fourierdlem62  46614  fourierdlem80  46632  fourierdlem97  46649  carageniuncllem2  46968  0ome  46975  fcoresf1  47529  fcoresfo  47531  fundcmpsurinjimaid  47883  isubgruhgr  48356  lindslinindimp2lem2  48947  zlmodzxzldeplem1  48988  line2  49240