Theorem sbf 2368

Description: Substitution for a variable not free in a wff does not affect it. (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 2367	. 2 ⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 195  Ⅎwnf 1699  [wsb 1867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701  df-sb 1868

This theorem is referenced by:  sbh  2369  sbf2  2370  nfs1f  2371  sb6x  2372  sbequ5  2375  sbequ6  2376  sbrim  2384  sblim  2385  sbrbif  2394  sbie  2396  sbid2  2401  equsb3  2420  sbcom4  2434  sbabel  2779  nfcdeq  3399  mo5f  28708  iuninc  28761  suppss2f  28819  fmptdF  28836  disjdsct  28863  esumpfinvalf  29465  measiuns  29607  ballotlemodife  29886  bj-sbf3  32014  bj-sbf4  32015  bj-sbieOLD  32020  mptsnunlem  32361  wl-equsb3  32516  ellimcabssub0  38684