Theorem sbf 2271

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1783  [wsb 2064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-sb 2065

This theorem is referenced by:  sbf2  2272  sbh  2273  nfs1f  2275  sbrimOLD  2305  sblim  2306  sbrbif  2311  sbiev  2314  sb8f  2356  sb6x  2469  sbequ5  2470  sbequ6  2471  sb2ae  2501  sbie  2507  sbid2  2513  sbabel  2938  sbabelOLD  2939  sbhypf  3544  nfcdeq  3783  mo5f  32508  suppss2f  32648  fmptdF  32666  disjdsct  32712  esumpfinvalf  34077  bj-sbf3  36840  bj-sbf4  36841  ellimcabssub0  45632  2reu8i  47125  ichf  47437