Theorem sbf 2277

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1784  [wsb 2067

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 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-sb 2068

This theorem is referenced by:  sbf2  2278  sbh  2279  nfs1f  2281  sblim  2311  sbrbif  2316  sbiev  2319  sb8f  2358  sb6x  2468  sbequ5  2469  sbequ6  2470  sb2ae  2500  sbie  2506  sbid2  2512  sbabel  2931  sbhypf  3502  nfcdeq  3735  mo5f  32563  suppss2f  32716  fmptdF  32734  disjdsct  32782  esumpfinvalf  34233  bj-sbf3  37040  bj-sbf4  37041  ellimcabssub0  45859  2reu8i  47355  ichf  47692