Theorem sbf 2278

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1785  [wsb 2068

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 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-sb 2069

This theorem is referenced by:  sbf2  2279  sbh  2280  nfs1f  2282  sblim  2312  sbrbif  2317  sbiev  2320  sb8f  2359  sb6x  2469  sbequ5  2470  sbequ6  2471  sb2ae  2501  sbie  2507  sbid2  2513  sbabel  2932  sbhypf  3504  nfcdeq  3737  mo5f  32574  suppss2f  32727  fmptdF  32745  disjdsct  32792  esumpfinvalf  34253  bj-sbf3  37081  bj-sbf4  37082  ellimcabssub0  45971  2reu8i  47467  ichf  47804