Theorem sbf 2275

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1784  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-sb 2068

This theorem is referenced by:  sbf2  2276  sbh  2277  nfs1f  2279  sblim  2309  sbrbif  2314  sbiev  2317  sb8f  2356  sb6x  2466  sbequ5  2467  sbequ6  2468  sb2ae  2498  sbie  2504  sbid2  2510  sbabel  2928  sbhypf  3499  nfcdeq  3732  mo5f  32470  suppss2f  32622  fmptdF  32640  disjdsct  32688  esumpfinvalf  34110  bj-sbf3  36904  bj-sbf4  36905  ellimcabssub0  45742  2reu8i  47238  ichf  47575