Theorem sbf 2304

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

Syntax hints:   ↔ wb 208  Ⅎwnf 1802  [wsb 2089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803  df-sb 2090

This theorem is referenced by:  sbf2  2305  sbh  2306  nfs1f  2308  sblim  2338  sbrbif  2343  sbiev  2345  sb8f  2384  sb6x  2494  sbequ5  2495  sbequ6  2496  sb2ae  2526  sbie  2532  sbid2  2538  sbabel  2955  sbhypf  3512  nfcdeq  3739  mo5f  32636  suppss2f  32790  fmptdF  32808  disjdsct  32855  esumpfinvalf  34334  bj-sbf3  37288  bj-sbf4  37289  ellimcabssub0  46157  2reu8i  47671  ichf  48020