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

This proof depends on syntax axioms:   ↔ wb 209  Ⅎwnf 1815  [wsb 2098

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-sb 2099

This theorem is used by:  sbf2  2305  sbh  2306  nfs1f  2308  sblim  2338  sbrbif  2343  sbiev  2345  sb8f  2383  sb6x  2493  sbequ5  2494  sbequ6  2495  sb2ae  2525  sbie  2531  sbid2  2537  sbabel  2954  sbhypf  3509  nfcdeq  3734  mo5f  33133  suppss2f  33280  fmptdf2  33298  disjdsct  33344  esumpfinvalf  34755  bj-sbf3  37844  bj-sbf4  37845  ellimcabssub0  46723  2reu8i  48277  ichf  48626