Theorem sbf 2257

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 2083. (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 2256	. 2 ⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 205  Ⅎwnf 1777  [wsb 2059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778  df-sb 2060

This theorem is referenced by:  sbf2  2258  sbh  2259  nfs1f  2261  sbrimOLD  2294  sblim  2295  sbrbif  2300  sb8f  2343  sb6x  2457  sbequ5  2458  sbequ6  2459  sb2ae  2489  sbie  2495  sbid2  2501  sbabel  2927  sbabelOLD  2928  sbhypf  3528  nfcdeq  3769  mo5f  32365  suppss2f  32505  fmptdF  32523  disjdsct  32564  esumpfinvalf  33826  bj-sbf3  36447  bj-sbf4  36448  ellimcabssub0  45143  2reu8i  46631  ichf  46927