Theorem sbf 2308

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

Syntax hints:   ↔ wb 209  Ⅎwnf 1806  [wsb 2093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807  df-sb 2094

This theorem is referenced by:  sbf2  2309  sbh  2310  nfs1f  2312  sblim  2342  sbrbif  2347  sbiev  2349  sb8f  2388  sb6x  2498  sbequ5  2499  sbequ6  2500  sb2ae  2530  sbie  2536  sbid2  2542  sbabel  2959  sbhypf  3516  nfcdeq  3743  mo5f  32745  suppss2f  32895  fmptdF  32913  disjdsct  32960  esumpfinvalf  34383  bj-sbf3  37336  bj-sbf4  37337  ellimcabssub0  46191  2reu8i  47705  ichf  48054