Theorem sbf 2263

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

Syntax hints:   ↔ wb 205  Ⅎwnf 1785  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786  df-sb 2068

This theorem is referenced by:  sbf2  2264  sbh  2265  nfs1f  2267  sbrimOLD  2302  sblim  2303  sbrbif  2308  sb8f  2350  sb6x  2463  sbequ5  2464  sbequ6  2465  sb2ae  2499  sbie  2505  sbid2  2511  sbabel  2939  sbabelOLD  2940  nfcdeq  3727  mo5f  31124  suppss2f  31259  fmptdF  31278  disjdsct  31320  esumpfinvalf  32340  bj-sbf3  35158  bj-sbf4  35159  ellimcabssub0  43544  2reu8i  45021  ichf  45318