Theorem feq1i 6708

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

Syntax hints:   ↔ wb 205   = wceq 1540  ⟶wf 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-fun 6545  df-fn 6546  df-f 6547

This theorem is referenced by:  ftpg  7156  fpropnf1  7269  suppsnop  8168  seqomlem2  8457  addnqf  10949  mulnqf  10950  isumsup2  15799  ruclem6  16185  sadcf  16401  sadadd2lem  16407  sadadd3  16409  sadaddlem  16414  smupf  16426  algrf  16517  funcoppc  17832  pmtr3ncomlem1  19386  znf1o  21330  ovolfsf  25233  ovolsf  25234  ovoliunlem1  25264  ovoliun  25267  ovoliun2  25268  voliunlem3  25314  itgss3  25577  dvexp  25718  efcn  26206  gamf  26798  basellem9  26844  axlowdimlem10  28491  wlkres  29209  1wlkdlem1  29672  vsfval  30168  ho0f  31286  opsqrlem4  31678  pjinvari  31726  fmptdF  32163  omssubaddlem  33611  omssubadd  33612  sitgclg  33654  sitgaddlemb  33660  coinfliprv  33794  plymul02  33870  signshf  33912  circum  34972  knoppcnlem8  35692  knoppcnlem11  35695  poimirlem31  36835  diophren  41866  clsf2  43192  seff  43383  binomcxplemnotnn0  43430  volicoff  45022  fourierdlem62  45195  fourierdlem80  45213  fourierdlem97  45230  carageniuncllem2  45549  0ome  45556  fcoresf1  46090  fcoresfo  46092  fundcmpsurinjimaid  46390  lindslinindimp2lem2  47240  zlmodzxzldeplem1  47281  line2  47538