Theorem nfsb 2155

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

Syntax hints:   A.wal 1368   F/wnf 1590   [wsb 1702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-sb 1703

This theorem is referenced by:  hbsb  2156  2sb5rfOLD  2170  2sb6rfOLD  2171  sb10f  2175  2sb8e  2189  sb8eu  2301  sb8euOLD  2302  sb8euOLDOLD  2303  2mo  2369  2moOLD  2370  2moOLDOLD  2371  2eu6OLD  2381  cbvabOLD  2596  cbvralf  3047  cbvreu  3051  cbvralsv  3064  cbvrexsv  3065  cbvrab  3076  cbvreucsf  3432  cbvrabcsf  3433  cbvopab1  4473  cbvmpt  4493  ralxpf  5097  cbviota  5497  sb8iota  5499  cbvriota  6174  dfoprab4f  6745  mo5f  26047  cbvmptf  26149  2sb5nd  31624  ax11-pm2  32701