Theorem sbf 2268

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

Syntax hints:   ↔ wb 209  Ⅎwnf 1785  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786  df-sb 2070

This theorem is referenced by:  sbf2  2269  sbh  2270  nfs1f  2272  sbbibOLD  2285  sbrim  2309  sblim  2311  sbrbif  2316  sb6x  2476  sbequ5  2477  sbequ6  2478  sb2ae  2514  sbie  2521  sbid2  2527  sbabel  2986  nfcdeq  3716  mo5f  30260  suppss2f  30398  fmptdF  30419  disjdsct  30462  esumpfinvalf  31445  bj-sbf3  34277  bj-sbf4  34278  ellimcabssub0  42259  2reu8i  43669  ichf  43967