Theorem feq1i 6682

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  ftpg  7131  fpropnf1  7245  suppsnop  8160  seqomlem2  8422  addnqf  10908  mulnqf  10909  isumsup2  15819  ruclem6  16210  sadcf  16430  sadadd2lem  16436  sadadd3  16438  sadaddlem  16443  smupf  16455  algrf  16550  funcoppc  17844  pmtr3ncomlem1  19410  znf1o  21468  ovolfsf  25379  ovolsf  25380  ovoliunlem1  25410  ovoliun  25413  ovoliun2  25414  voliunlem3  25460  itgss3  25723  dvexp  25864  efcn  26360  gamf  26960  basellem9  27006  axlowdimlem10  28885  wlkres  29605  1wlkdlem1  30073  vsfval  30569  ho0f  31687  opsqrlem4  32079  pjinvari  32127  fmptdF  32587  omssubaddlem  34297  omssubadd  34298  sitgclg  34340  sitgaddlemb  34346  coinfliprv  34481  plymul02  34544  signshf  34586  circum  35668  knoppcnlem8  36495  knoppcnlem11  36498  poimirlem31  37652  diophren  42808  clsf2  44122  seff  44305  binomcxplemnotnn0  44352  volicoff  46000  fourierdlem62  46173  fourierdlem80  46191  fourierdlem97  46208  carageniuncllem2  46527  0ome  46534  fcoresf1  47074  fcoresfo  47076  fundcmpsurinjimaid  47416  isubgruhgr  47872  lindslinindimp2lem2  48452  zlmodzxzldeplem1  48493  line2  48745