Theorem sbf 2262

Description: Substitution for a variable not free in a wff does not affect it. For a version requiring disjoint variables but fewer axioms, see sbv 2091. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)

Hypothesis

Ref	Expression
sbf.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
sbf	⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)

Proof of Theorem sbf

Step	Hyp	Ref	Expression
1		sbf.1	. 2 ⊢ Ⅎ𝑥𝜑
2		sbft 2261	. 2 ⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 205  Ⅎwnf 1785  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786  df-sb 2068

This theorem is referenced by:  sbf2  2263  sbh  2264  nfs1f  2266  sbrimOLD  2301  sblim  2302  sbrbif  2307  sb8f  2349  sb6x  2462  sbequ5  2463  sbequ6  2464  sb2ae  2494  sbie  2500  sbid2  2506  sbabel  2937  sbabelOLD  2938  sbhypf  3508  nfcdeq  3738  mo5f  31481  suppss2f  31620  fmptdF  31639  disjdsct  31684  esumpfinvalf  32764  bj-sbf3  35380  bj-sbf4  35381  ellimcabssub0  43978  2reu8i  45465  ichf  45762