Theorem sbf 2380

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	|- F/ x ph

Assertion

Ref	Expression
sbf	|- ( [ y / x ] ph <-> ph )

Proof of Theorem sbf

Step	Hyp	Ref	Expression
1		sbf.1	. 2 |- F/ x ph
2		sbft 2379	. 2 |- ( F/ x ph -> ( [ y / x ] ph <-> ph ) )
3	1, 2	ax-mp 5	1 |- ( [ y / x ] ph <-> ph )

Syntax hints:   <-> wb 196   F/wnf 1708   [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-nf 1710  df-sb 1881

This theorem is referenced by:  sbh  2381  sbf2  2382  nfs1f  2383  sb6x  2384  sbequ5  2387  sbequ6  2388  sbrim  2396  sblim  2397  sbrbif  2406  sbie  2408  sbid2  2413  equsb3  2432  sbcom4  2446  sbabel  2793  nfcdeq  3432  mo5f  29324  iuninc  29379  suppss2f  29439  fmptdF  29456  disjdsct  29480  esumpfinvalf  30138  measiuns  30280  ballotlemodife  30559  bj-sbf3  32826  bj-sbf4  32827  mptsnunlem  33185  wl-equsb3  33337  ellimcabssub0  39849