Theorem feq1i 6728

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

Syntax hints:   ↔ wb 206   = wceq 1537  ⟶wf 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-fun 6565  df-fn 6566  df-f 6567

This theorem is referenced by:  ftpg  7176  fpropnf1  7287  suppsnop  8202  seqomlem2  8490  addnqf  10986  mulnqf  10987  isumsup2  15879  ruclem6  16268  sadcf  16487  sadadd2lem  16493  sadadd3  16495  sadaddlem  16500  smupf  16512  algrf  16607  funcoppc  17926  pmtr3ncomlem1  19506  znf1o  21588  ovolfsf  25520  ovolsf  25521  ovoliunlem1  25551  ovoliun  25554  ovoliun2  25555  voliunlem3  25601  itgss3  25865  dvexp  26006  efcn  26502  gamf  27101  basellem9  27147  axlowdimlem10  28981  wlkres  29703  1wlkdlem1  30166  vsfval  30662  ho0f  31780  opsqrlem4  32172  pjinvari  32220  fmptdF  32673  omssubaddlem  34281  omssubadd  34282  sitgclg  34324  sitgaddlemb  34330  coinfliprv  34464  plymul02  34540  signshf  34582  circum  35659  knoppcnlem8  36483  knoppcnlem11  36486  poimirlem31  37638  diophren  42801  clsf2  44116  seff  44305  binomcxplemnotnn0  44352  volicoff  45951  fourierdlem62  46124  fourierdlem80  46142  fourierdlem97  46159  carageniuncllem2  46478  0ome  46485  fcoresf1  47019  fcoresfo  47021  fundcmpsurinjimaid  47336  isubgruhgr  47792  lindslinindimp2lem2  48305  zlmodzxzldeplem1  48346  line2  48602