Theorem feq1i 6678

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

Syntax hints:   ↔ wb 208   = wceq 1559  ⟶wf 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-fun 6519  df-fn 6520  df-f 6521

This theorem is referenced by:  ftpg  7135  fpropnf1  7247  suppsnop  8153  seqomlem2  8417  addnqf  10903  mulnqf  10904  isumsup2  15859  ruclem6  16250  sadcf  16470  sadadd2lem  16476  sadadd3  16478  sadaddlem  16483  smupf  16495  algrf  16590  funcoppc  17891  pmtr3ncomlem1  19496  znf1o  21583  ovolfsf  25513  ovolsf  25514  ovoliunlem1  25544  ovoliun  25547  ovoliun2  25548  voliunlem3  25594  itgss3  25857  dvexp  25995  efcn  26483  gamf  27084  basellem9  27130  axlowdimlem10  29098  wlkres  29815  1wlkdlem1  30285  vsfval  30782  ho0f  31900  opsqrlem4  32292  pjinvari  32340  fmptdF  32808  mplmulmvr  33797  omssubaddlem  34557  omssubadd  34558  sitgclg  34600  sitgaddlemb  34606  coinfliprv  34741  plymul02  34804  signshf  34846  circum  35988  knoppcnlem8  36902  knoppcnlem11  36905  poimirlem31  38114  diophren  43354  clsf2  44666  seff  44849  binomcxplemnotnn0  44896  volicoff  46533  fourierdlem62  46706  fourierdlem80  46724  fourierdlem97  46741  carageniuncllem2  47060  0ome  47067  fcoresf1  47627  fcoresfo  47629  fundcmpsurinjimaid  47981  isubgruhgr  48454  lindslinindimp2lem2  49045  zlmodzxzldeplem1  49086  line2  49338