Theorem feq1i 6478

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

Syntax hints:   ↔ wb 209   = wceq 1538  ⟶wf 6320

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-fun 6326  df-fn 6327  df-f 6328

This theorem is referenced by:  ftpg  6895  fpropnf1  7003  suppsnop  7827  seqomlem2  8070  addnqf  10359  mulnqf  10360  isumsup2  15193  ruclem6  15580  sadcf  15792  sadadd2lem  15798  sadadd3  15800  sadaddlem  15805  smupf  15817  algrf  15907  funcoppc  17137  pmtr3ncomlem1  18593  znf1o  20243  ovolfsf  24075  ovolsf  24076  ovoliunlem1  24106  ovoliun  24109  ovoliun2  24110  voliunlem3  24156  itgss3  24418  dvexp  24556  efcn  25038  gamf  25628  basellem9  25674  axlowdimlem10  26745  wlkres  27460  1wlkdlem1  27922  vsfval  28416  ho0f  29534  opsqrlem4  29926  pjinvari  29974  fmptdF  30419  omssubaddlem  31667  omssubadd  31668  sitgclg  31710  sitgaddlemb  31716  coinfliprv  31850  plymul02  31926  signshf  31968  circum  33030  knoppcnlem8  33952  knoppcnlem11  33955  poimirlem31  35088  diophren  39754  clsf2  40829  seff  41013  binomcxplemnotnn0  41060  volicoff  42637  fourierdlem62  42810  fourierdlem80  42828  fourierdlem97  42845  carageniuncllem2  43161  0ome  43168  fundcmpsurinjimaid  43928  lindslinindimp2lem2  44868  zlmodzxzldeplem1  44909  line2  45166