Theorem sbf 2273

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 2272	. 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 2180

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

This theorem is referenced by:  sbf2  2274  sbh  2275  nfs1f  2277  sblim  2307  sbrbif  2312  sbiev  2315  sb8f  2354  sb6x  2464  sbequ5  2465  sbequ6  2466  sb2ae  2496  sbie  2502  sbid2  2508  sbabel  2927  sbhypf  3499  nfcdeq  3736  mo5f  32466  suppss2f  32618  fmptdF  32636  disjdsct  32682  esumpfinvalf  34087  bj-sbf3  36879  bj-sbf4  36880  ellimcabssub0  45663  2reu8i  47150  ichf  47487