Theorem sbf 2282

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

Syntax hints:   ↔ wb 207  Ⅎwnf 1790  [wsb 2073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-sb 2074

This theorem is referenced by:  sbf2  2283  sbh  2284  nfs1f  2286  sblim  2316  sbrbif  2321  sbiev  2323  sb8f  2362  sb6x  2472  sbequ5  2473  sbequ6  2474  sb2ae  2504  sbie  2510  sbid2  2516  sbabel  2934  sbhypf  3493  nfcdeq  3725  mo5f  32583  suppss2f  32737  fmptdF  32755  disjdsct  32802  esumpfinvalf  34267  bj-sbf3  37199  bj-sbf4  37200  ellimcabssub0  46069  2reu8i  47583  ichf  47932