Theorem sbf 2268

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1779  [wsb 2061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-ex 1776  df-nf 1780  df-sb 2062

This theorem is referenced by:  sbf2  2269  sbh  2270  nfs1f  2272  sbrimOLD  2303  sblim  2304  sbrbif  2309  sbiev  2312  sb8f  2353  sb6x  2466  sbequ5  2467  sbequ6  2468  sb2ae  2498  sbie  2504  sbid2  2510  sbabel  2935  sbabelOLD  2936  sbhypf  3543  nfcdeq  3785  mo5f  32516  suppss2f  32654  fmptdF  32672  disjdsct  32717  esumpfinvalf  34056  bj-sbf3  36821  bj-sbf4  36822  ellimcabssub0  45572  2reu8i  47062  ichf  47374