Theorem sbf 2266

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

Syntax hints:   ↔ wb 205  Ⅎwnf 1787  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788  df-sb 2069

This theorem is referenced by:  sbf2  2267  sbh  2268  nfs1f  2270  sbrim  2304  sblim  2306  sbrbif  2311  sb6x  2464  sbequ5  2465  sbequ6  2466  sb2ae  2500  sbie  2506  sbid2  2512  sbabel  2940  sbabelOLD  2941  nfcdeq  3707  mo5f  30738  suppss2f  30875  fmptdF  30895  disjdsct  30937  esumpfinvalf  31944  bj-sbf3  34949  bj-sbf4  34950  ellimcabssub0  43048  2reu8i  44492  ichf  44790