Theorem feq1i 6659

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

Syntax hints:   ↔ wb 206   = wceq 1542  ⟶wf 6494

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6500  df-fn 6501  df-f 6502

This theorem is referenced by:  ftpg  7110  fpropnf1  7222  suppsnop  8128  seqomlem2  8390  addnqf  10871  mulnqf  10872  isumsup2  15811  ruclem6  16202  sadcf  16422  sadadd2lem  16428  sadadd3  16430  sadaddlem  16435  smupf  16447  algrf  16542  funcoppc  17842  pmtr3ncomlem1  19448  znf1o  21531  ovolfsf  25438  ovolsf  25439  ovoliunlem1  25469  ovoliun  25472  ovoliun2  25473  voliunlem3  25519  itgss3  25782  dvexp  25920  efcn  26408  gamf  27006  basellem9  27052  axlowdimlem10  29020  wlkres  29737  1wlkdlem1  30207  vsfval  30704  ho0f  31822  opsqrlem4  32214  pjinvari  32262  fmptdF  32729  mplmulmvr  33683  omssubaddlem  34443  omssubadd  34444  sitgclg  34486  sitgaddlemb  34492  coinfliprv  34627  plymul02  34690  signshf  34732  circum  35856  knoppcnlem8  36760  knoppcnlem11  36763  poimirlem31  37972  diophren  43241  clsf2  44553  seff  44736  binomcxplemnotnn0  44783  volicoff  46423  fourierdlem62  46596  fourierdlem80  46614  fourierdlem97  46631  carageniuncllem2  46950  0ome  46957  fcoresf1  47517  fcoresfo  47519  fundcmpsurinjimaid  47871  isubgruhgr  48344  lindslinindimp2lem2  48935  zlmodzxzldeplem1  48976  line2  49228