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  3017  nfcdeq  3770  mo5f  30255  suppss2f  30386  fmptdF  30403  disjdsct  30440  esumpfinvalf  31337  bj-sbf3  34164  bj-sbf4  34165  ellimcabssub0  41905  2reu8i  43319  ichf  43617