Theorem feq1i 6335

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

Syntax hints:   ↔ wb 198   = wceq 1507  ⟶wf 6184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-br 4930  df-opab 4992  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-fun 6190  df-fn 6191  df-f 6192

This theorem is referenced by:  ftpg  6741  fpropnf1  6850  suppsnop  7647  seqomlem2  7890  addnqf  10168  mulnqf  10169  isumsup2  15061  ruclem6  15448  sadcf  15662  sadadd2lem  15668  sadadd3  15670  sadaddlem  15675  smupf  15687  algrf  15773  funcoppc  17003  pmtr3ncomlem1  18362  znf1o  20400  ovolfsf  23775  ovolsf  23776  ovoliunlem1  23806  ovoliun  23809  ovoliun2  23810  voliunlem3  23856  itgss3  24118  dvexp  24253  efcn  24734  gamf  25322  basellem9  25368  axlowdimlem10  26440  wlkres  27156  wlkresOLD  27158  1wlkdlem1  27666  vsfval  28187  ho0f  29309  opsqrlem4  29701  pjinvari  29749  fmptdF  30163  omssubaddlem  31208  omssubadd  31209  sitgclg  31251  sitgaddlemb  31257  coinfliprv  31392  plymul02  31468  signshf  31512  circum  32443  knoppcnlem8  33365  knoppcnlem11  33368  poimirlem31  34370  diophren  38812  clsf2  39845  seff  40063  binomcxplemnotnn0  40110  volicoff  41717  fourierdlem62  41890  fourierdlem80  41908  fourierdlem97  41925  carageniuncllem2  42241  0ome  42248  mapprop  43764  lindslinindimp2lem2  43887  zlmodzxzldeplem1  43928  line2  44113