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

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

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 1914  ax-6 1972  ax-7 2012  ax-12 2172

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

This theorem is referenced by:  sbf2  2264  sbh  2265  nfs1f  2267  sbrimOLD  2302  sblim  2303  sbrbif  2308  sb8f  2350  sb6x  2464  sbequ5  2465  sbequ6  2466  sb2ae  2496  sbie  2502  sbid2  2508  sbabel  2939  sbabelOLD  2940  sbhypf  3539  nfcdeq  3774  mo5f  31729  suppss2f  31863  fmptdF  31881  disjdsct  31924  esumpfinvalf  33074  bj-sbf3  35717  bj-sbf4  35718  ellimcabssub0  44333  2reu8i  45821  ichf  46118