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

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

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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  sbf2  2309  sbh  2310  nfs1f  2312  sblim  2342  sbrbif  2347  sbiev  2349  sb8f  2386  sb6x  2496  sbequ5  2497  sbequ6  2498  sb2ae  2528  sbie  2534  sbid2  2540  sbabel  2958  sbhypf  3513  nfcdeq  3738  mo5f  33160  suppss2f  33307  fmptdf2  33325  disjdsct  33370  esumpfinvalf  34791  bj-sbf3  37942  bj-sbf4  37943  ellimcabssub0  46844  2reu8i  48399  ichf  48747