Theorem feq1i 6679

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

Syntax hints:   ↔ wb 206   = wceq 1540  ⟶wf 6507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  ftpg  7128  fpropnf1  7242  suppsnop  8157  seqomlem2  8419  addnqf  10901  mulnqf  10902  isumsup2  15812  ruclem6  16203  sadcf  16423  sadadd2lem  16429  sadadd3  16431  sadaddlem  16436  smupf  16448  algrf  16543  funcoppc  17837  pmtr3ncomlem1  19403  znf1o  21461  ovolfsf  25372  ovolsf  25373  ovoliunlem1  25403  ovoliun  25406  ovoliun2  25407  voliunlem3  25453  itgss3  25716  dvexp  25857  efcn  26353  gamf  26953  basellem9  26999  axlowdimlem10  28878  wlkres  29598  1wlkdlem1  30066  vsfval  30562  ho0f  31680  opsqrlem4  32072  pjinvari  32120  fmptdF  32580  omssubaddlem  34290  omssubadd  34291  sitgclg  34333  sitgaddlemb  34339  coinfliprv  34474  plymul02  34537  signshf  34579  circum  35661  knoppcnlem8  36488  knoppcnlem11  36491  poimirlem31  37645  diophren  42801  clsf2  44115  seff  44298  binomcxplemnotnn0  44345  volicoff  45993  fourierdlem62  46166  fourierdlem80  46184  fourierdlem97  46201  carageniuncllem2  46520  0ome  46527  fcoresf1  47070  fcoresfo  47072  fundcmpsurinjimaid  47412  isubgruhgr  47868  lindslinindimp2lem2  48448  zlmodzxzldeplem1  48489  line2  48741