Theorem feq1i 6702

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  ftpg  7151  fpropnf1  7265  suppsnop  8182  seqomlem2  8470  addnqf  10967  mulnqf  10968  isumsup2  15867  ruclem6  16258  sadcf  16477  sadadd2lem  16483  sadadd3  16485  sadaddlem  16490  smupf  16502  algrf  16597  funcoppc  17893  pmtr3ncomlem1  19459  znf1o  21517  ovolfsf  25429  ovolsf  25430  ovoliunlem1  25460  ovoliun  25463  ovoliun2  25464  voliunlem3  25510  itgss3  25773  dvexp  25914  efcn  26410  gamf  27010  basellem9  27056  axlowdimlem10  28935  wlkres  29655  1wlkdlem1  30123  vsfval  30619  ho0f  31737  opsqrlem4  32129  pjinvari  32177  fmptdF  32639  omssubaddlem  34336  omssubadd  34337  sitgclg  34379  sitgaddlemb  34385  coinfliprv  34520  plymul02  34583  signshf  34625  circum  35701  knoppcnlem8  36523  knoppcnlem11  36526  poimirlem31  37680  diophren  42803  clsf2  44117  seff  44300  binomcxplemnotnn0  44347  volicoff  45991  fourierdlem62  46164  fourierdlem80  46182  fourierdlem97  46199  carageniuncllem2  46518  0ome  46525  fcoresf1  47065  fcoresfo  47067  fundcmpsurinjimaid  47392  isubgruhgr  47848  lindslinindimp2lem2  48402  zlmodzxzldeplem1  48443  line2  48699