Theorem feq1i 6698

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

Syntax hints:   ↔ wb 209   = wceq 1570  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  ftpg  7155  fpropnf1  7267  suppsnop  8175  seqomlem2  8439  addnqf  10934  mulnqf  10935  isumsup2  15902  ruclem6  16292  sadcf  16512  sadadd2lem  16518  sadadd3  16520  sadaddlem  16525  smupf  16537  algrf  16632  funcoppc  17933  pmtr3ncomlem1  19544  znf1o  21682  ovolfsf  25611  ovolsf  25612  ovoliunlem1  25642  ovoliun  25645  ovoliun2  25646  voliunlem3  25692  itgss3  25955  dvexp  26093  plymul02  26422  efcn  26584  gamf  27185  basellem9  27231  axlowdimlem10  29279  wlkres  29996  1wlkdlem1  30466  vsfval  30963  ho0f  32081  opsqrlem4  32473  pjinvari  32521  fmptdF  32979  mplmulmvr  33907  omssubaddlem  34667  omssubadd  34668  sitgclg  34710  sitgaddlemb  34716  coinfliprv  34851  signshf  34953  circum  36144  knoppcnlem8  37067  knoppcnlem11  37070  poimirlem31  38280  diophren  43520  clsf2  44832  seff  44999  binomcxplemnotnn0  45046  volicoff  46689  fourierdlem62  46862  fourierdlem80  46880  fourierdlem97  46897  carageniuncllem2  47216  0ome  47223  fcoresf1  47783  fcoresfo  47785  fundcmpsurinjimaid  48137  isubgruhgr  48610  lindslinindimp2lem2  49216  zlmodzxzldeplem1  49257  line2  49509