Theorem feq1i 6036

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

Syntax hints:   ↔ wb 196   = wceq 1483  ⟶wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-fun 5890  df-fn 5891  df-f 5892

This theorem is referenced by:  ftpg  6423  fpropnf1  6524  suppsnop  7309  seqomlem2  7546  addnqf  9770  mulnqf  9771  hashfOLD  13126  isumsup2  14578  ruclem6  14964  sadcf  15175  sadadd2lem  15181  sadadd3  15183  sadaddlem  15188  smupf  15200  algrf  15286  funcoppc  16535  pmtr3ncomlem1  17893  znf1o  19900  ovolfsf  23240  ovolsf  23241  ovoliunlem1  23270  ovoliun  23273  ovoliun2  23274  voliunlem3  23320  itgss3  23581  dvexp  23716  efcn  24197  gamf  24769  basellem9  24815  axlowdimlem10  25831  wlkres  26567  1wlkdlem1  26997  vsfval  27488  ho0f  28610  opsqrlem4  29002  pjinvari  29050  fmptdF  29456  omssubaddlem  30361  omssubadd  30362  sitgclg  30404  sitgaddlemb  30410  coinfliprv  30544  plymul02  30623  signshf  30665  circum  31568  knoppcnlem8  32490  knoppcnlem11  32493  poimirlem31  33440  diophren  37377  clsf2  38424  seff  38508  binomcxplemnotnn0  38555  volicoff  40212  fourierdlem62  40385  fourierdlem80  40403  fourierdlem97  40420  carageniuncllem2  40736  0ome  40743  mapprop  42124  lindslinindimp2lem2  42248  zlmodzxzldeplem1  42289