Theorem sbf 2272

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1781  [wsb 2064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782  df-sb 2065

This theorem is referenced by:  sbf2  2273  sbh  2274  nfs1f  2276  sbrimOLD  2309  sblim  2310  sbrbif  2315  sbiev  2318  sb8f  2359  sb6x  2472  sbequ5  2473  sbequ6  2474  sb2ae  2504  sbie  2510  sbid2  2516  sbabel  2944  sbabelOLD  2945  sbhypf  3556  nfcdeq  3799  mo5f  32517  suppss2f  32657  fmptdF  32674  disjdsct  32714  esumpfinvalf  34040  bj-sbf3  36805  bj-sbf4  36806  ellimcabssub0  45538  2reu8i  47028  ichf  47324