Theorem sbf 2309

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 2308	. 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 2216

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  2310  sbh  2311  nfs1f  2313  sblim  2343  sbrbif  2348  sbiev  2350  sb8f  2389  sb6x  2499  sbequ5  2500  sbequ6  2501  sb2ae  2531  sbie  2537  sbid2  2543  sbabel  2960  sbhypf  3517  nfcdeq  3743  mo5f  32872  suppss2f  33020  fmptdf2  33038  disjdsct  33085  esumpfinvalf  34497  bj-sbf3  37515  bj-sbf4  37516  ellimcabssub0  46374  2reu8i  47891  ichf  48240