Theorem feq1i 6686

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

Syntax hints:   ↔ wb 209   = wceq 1563  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-fun 6527  df-fn 6528  df-f 6529

This theorem is referenced by:  ftpg  7143  fpropnf1  7255  suppsnop  8162  seqomlem2  8426  addnqf  10921  mulnqf  10922  isumsup2  15890  ruclem6  16281  sadcf  16501  sadadd2lem  16507  sadadd3  16509  sadaddlem  16514  smupf  16526  algrf  16621  funcoppc  17922  pmtr3ncomlem1  19534  znf1o  21661  ovolfsf  25591  ovolsf  25592  ovoliunlem1  25622  ovoliun  25625  ovoliun2  25626  voliunlem3  25672  itgss3  25935  dvexp  26073  plymul02  26402  efcn  26564  gamf  27165  basellem9  27211  axlowdimlem10  29210  wlkres  29927  1wlkdlem1  30397  vsfval  30894  ho0f  32012  opsqrlem4  32404  pjinvari  32452  fmptdF  32913  mplmulmvr  33846  omssubaddlem  34606  omssubadd  34607  sitgclg  34649  sitgaddlemb  34655  coinfliprv  34790  signshf  34892  circum  36037  knoppcnlem8  36951  knoppcnlem11  36954  poimirlem31  38162  diophren  43402  clsf2  44714  seff  44883  binomcxplemnotnn0  44930  volicoff  46567  fourierdlem62  46740  fourierdlem80  46758  fourierdlem97  46775  carageniuncllem2  47094  0ome  47101  fcoresf1  47661  fcoresfo  47663  fundcmpsurinjimaid  48015  isubgruhgr  48488  lindslinindimp2lem2  49090  zlmodzxzldeplem1  49131  line2  49383