Theorem sbf 2271

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1783  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-sb 2066

This theorem is referenced by:  sbf2  2272  sbh  2273  nfs1f  2275  sblim  2305  sbrbif  2310  sbiev  2313  sb8f  2352  sb6x  2462  sbequ5  2463  sbequ6  2464  sb2ae  2494  sbie  2500  sbid2  2506  sbabel  2924  sbhypf  3510  nfcdeq  3748  mo5f  32418  suppss2f  32562  fmptdF  32580  disjdsct  32626  esumpfinvalf  34066  bj-sbf3  36827  bj-sbf4  36828  ellimcabssub0  45615  2reu8i  47114  ichf  47451