Theorem nfsb 2148

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 2012	. 2 |- ( A. z z = y -> F/ z [ y / x ] ph )
2		nfsb.1	. . 3 |- F/ z ph
3	2	nfsb4 2079	. 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 1360   F/wnf 1592   [wsb 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700

This theorem is referenced by:  hbsb  2149  2sb5rfOLD  2163  2sb6rfOLD  2164  sb10f  2168  sb8eu  2289  sb8euOLD  2290  2mo  2355  2moOLD  2356  2eu6  2363  cbvab  2551  cbvralf  2931  cbvreu  2935  cbvralsv  2948  cbvrexsv  2949  cbvrab  2960  cbvreucsf  3309  cbvrabcsf  3310  cbvopab1  4350  cbvmpt  4370  ralxpf  4973  cbviota  5374  sb8iota  5376  cbvriota  6050  dfoprab4f  6621  mo5f  25692  cbvmptf  25795  2sb5nd  30991  ax11-pm2  31985