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 2098. (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 208  Ⅎwnf 1784  [wsb 2069

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 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-nf 1785  df-sb 2070

This theorem is referenced by:  sbf2  2272  sbh  2273  nfs1f  2275  sbbibOLD  2289  sbrim  2313  sblim  2315  sbrbif  2321  sbievOLD  2331  sb6x  2487  sbequ5  2488  sbequ6  2489  sb2ae  2536  sbie  2544  sbid2  2550  sbabel  3015  nfcdeq  3768  mo5f  30253  suppss2f  30384  fmptdF  30401  disjdsct  30438  esumpfinvalf  31335  bj-sbf3  34162  bj-sbf4  34163  ellimcabssub0  41918  2reu8i  43332  ichf  43630