Theorem sbf 2263

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

Syntax hints:   ↔ wb 205  Ⅎwnf 1786  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787  df-sb 2068

This theorem is referenced by:  sbf2  2264  sbh  2265  nfs1f  2267  sbrimOLD  2302  sblim  2303  sbrbif  2308  sb8f  2351  sb6x  2464  sbequ5  2465  sbequ6  2466  sb2ae  2500  sbie  2506  sbid2  2512  sbabel  2941  sbabelOLD  2942  nfcdeq  3712  mo5f  30837  suppss2f  30974  fmptdF  30993  disjdsct  31035  esumpfinvalf  32044  bj-sbf3  35022  bj-sbf4  35023  ellimcabssub0  43158  2reu8i  44605  ichf  44902