Theorem feq1i 6621

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

Syntax hints:   ↔ wb 205   = wceq 1539  ⟶wf 6454

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-fun 6460  df-fn 6461  df-f 6462

This theorem is referenced by:  ftpg  7060  fpropnf1  7172  suppsnop  8025  seqomlem2  8313  addnqf  10750  mulnqf  10751  isumsup2  15603  ruclem6  15989  sadcf  16205  sadadd2lem  16211  sadadd3  16213  sadaddlem  16218  smupf  16230  algrf  16323  funcoppc  17635  pmtr3ncomlem1  19126  znf1o  20804  ovolfsf  24680  ovolsf  24681  ovoliunlem1  24711  ovoliun  24714  ovoliun2  24715  voliunlem3  24761  itgss3  25024  dvexp  25162  efcn  25647  gamf  26237  basellem9  26283  axlowdimlem10  27364  wlkres  28083  1wlkdlem1  28546  vsfval  29040  ho0f  30158  opsqrlem4  30550  pjinvari  30598  fmptdF  31038  omssubaddlem  32311  omssubadd  32312  sitgclg  32354  sitgaddlemb  32360  coinfliprv  32494  plymul02  32570  signshf  32612  circum  33677  knoppcnlem8  34725  knoppcnlem11  34728  poimirlem31  35852  diophren  40672  clsf2  41774  seff  41965  binomcxplemnotnn0  42012  volicoff  43585  fourierdlem62  43758  fourierdlem80  43776  fourierdlem97  43793  carageniuncllem2  44110  0ome  44117  fcoresf1  44621  fcoresfo  44623  fundcmpsurinjimaid  44921  lindslinindimp2lem2  45858  zlmodzxzldeplem1  45899  line2  46156