Theorem nfsb 2269

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 2027	. 2 |- ( A. z z = y -> F/ z [ y / x ] ph )
2		nfsb.1	. . 3 |- F/ z ph
3	2	nfsb4 2219	. 2 |- ( -. A. z z = y -> F/ z [ y / x ] ph )
4	1, 3	pm2.61i 168	1 |- F/ z [ y / x ] ph

Syntax hints:   A.wal 1442   F/wnf 1667   [wsb 1797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668  df-sb 1798

This theorem is referenced by:  hbsb  2270  sb10f  2285  2sb8e  2296  sb8eu  2332  2mo  2380  cbvralf  3013  cbvreu  3017  cbvralsv  3030  cbvrexsv  3031  cbvrab  3043  cbvreucsf  3397  cbvrabcsf  3398  cbvopab1  4473  cbvmptf  4493  cbvmpt  4494  ralxpf  4981  cbviota  5551  sb8iota  5553  cbvriota  6262  dfoprab4f  6851  mo5f  28120  ax11-pm2  31438  2sb5nd  36927