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 2125. (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 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 209  Ⅎwnf 1816  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2215

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100

This theorem is used by:  sbf2  2307  sbh  2308  nfs1f  2310  sblim  2340  sbrbif  2345  sbiev  2347  sb8f  2385  sb6x  2495  sbequ5  2496  sbequ6  2497  sb2ae  2527  sbie  2533  sbid2  2539  sbabel  2956  sbhypf  3512  nfcdeq  3738  mo5f  32972  suppss2f  33119  fmptdf2  33137  disjdsct  33183  esumpfinvalf  34594  bj-sbf3  37590  bj-sbf4  37591  ellimcabssub0  46455  2reu8i  48009  ichf  48358