Theorem sbf 2305

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 2304	. 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 2213

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  2306  sbh  2307  nfs1f  2309  sblim  2339  sbrbif  2344  sbiev  2346  sb8f  2384  sb6x  2494  sbequ5  2495  sbequ6  2496  sb2ae  2526  sbie  2532  sbid2  2538  sbabel  2955  sbhypf  3510  nfcdeq  3735  mo5f  33067  suppss2f  33214  fmptdf2  33232  disjdsct  33278  esumpfinvalf  34690  bj-sbf3  37721  bj-sbf4  37722  ellimcabssub0  46573  2reu8i  48127  ichf  48476