Theorem nfsb 2440

Description: If z is not free in ph, it is not free in [ y / x ] ph when y and z are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfsb.1	|- F/ z ph

Assertion

Ref	Expression
nfsb	|- F/ z [ y / x ] ph

Distinct variable group:   y, z

Allowed substitution hints:   ph( x, y, z)

Proof of Theorem nfsb

Step	Hyp	Ref	Expression
1		axc16nf 2137	. 2 |- ( A. z z = y -> F/ z [ y / x ] ph )
2		nfsb.1	. . 3 |- F/ z ph
3	2	nfsb4 2390	. 2 |- ( -. A. z z = y -> F/ z [ y / x ] ph )
4	1, 3	pm2.61i 176	1 |- F/ z [ y / x ] ph

Syntax hints:   A.wal 1481   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-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

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

This theorem is referenced by:  hbsb  2441  sb10f  2456  2sb8e  2467  sb8eu  2503  2mo  2551  cbvralf  3165  cbvreu  3169  cbvralsv  3182  cbvrexsv  3183  cbvrab  3198  cbvreucsf  3567  cbvrabcsf  3568  cbvopab1  4723  cbvmptf  4748  cbvmpt  4749  ralxpf  5268  cbviota  5856  sb8iota  5858  cbvriota  6621  dfoprab4f  7226  mo5f  29324  ax11-pm2  32823  2sb5nd  38776