Theorem feq1i 6647

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

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

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  ftpg  7094  fpropnf1  7208  suppsnop  8118  seqomlem2  8380  addnqf  10861  mulnqf  10862  isumsup2  15771  ruclem6  16162  sadcf  16382  sadadd2lem  16388  sadadd3  16390  sadaddlem  16395  smupf  16407  algrf  16502  funcoppc  17800  pmtr3ncomlem1  19370  znf1o  21476  ovolfsf  25388  ovolsf  25389  ovoliunlem1  25419  ovoliun  25422  ovoliun2  25423  voliunlem3  25469  itgss3  25732  dvexp  25873  efcn  26369  gamf  26969  basellem9  27015  axlowdimlem10  28914  wlkres  29632  1wlkdlem1  30099  vsfval  30595  ho0f  31713  opsqrlem4  32105  pjinvari  32153  fmptdF  32613  omssubaddlem  34266  omssubadd  34267  sitgclg  34309  sitgaddlemb  34315  coinfliprv  34450  plymul02  34513  signshf  34555  circum  35646  knoppcnlem8  36473  knoppcnlem11  36476  poimirlem31  37630  diophren  42786  clsf2  44099  seff  44282  binomcxplemnotnn0  44329  volicoff  45977  fourierdlem62  46150  fourierdlem80  46168  fourierdlem97  46185  carageniuncllem2  46504  0ome  46511  fcoresf1  47054  fcoresfo  47056  fundcmpsurinjimaid  47396  isubgruhgr  47853  lindslinindimp2lem2  48445  zlmodzxzldeplem1  48486  line2  48738