Theorem sbf 2199

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

Syntax hints:   ↔ wb 198  Ⅎwnf 1746  [wsb 2015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-12 2106

This theorem depends on definitions:  df-bi 199  df-ex 1743  df-nf 1747  df-sb 2016

This theorem is referenced by:  sbf2  2200  sbh  2201  nfs1f  2204  sbbibOLD  2215  sbrim  2238  sblim  2239  sbrbif  2244  sbievOLD  2254  sb6x  2402  sbequ5  2403  sbequ6  2404  sb2ae  2457  sbie  2468  sbid2  2474  sbabel  2966  nfcdeq  3677  mo5f  30035  suppss2f  30146  fmptdF  30163  disjdsct  30197  esumpfinvalf  30985  bj-sbf3  33659  bj-sbf4  33660  ellimcabssub0  41335  2reu8i  42724