Theorem sbf 2306

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

Syntax hints:   ↔ wb 209  Ⅎwnf 1813  [wsb 2096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-sb 2097

This theorem is referenced by:  sbf2  2307  sbh  2308  nfs1f  2310  sblim  2340  sbrbif  2345  sbiev  2347  sb8f  2386  sb6x  2496  sbequ5  2497  sbequ6  2498  sb2ae  2528  sbie  2534  sbid2  2540  sbabel  2957  sbhypf  3514  nfcdeq  3741  mo5f  32816  suppss2f  32964  fmptdF  32982  disjdsct  33029  esumpfinvalf  34447  bj-sbf3  37455  bj-sbf4  37456  ellimcabssub0  46316  2reu8i  47833  ichf  48182