Theorem nfsb 2208

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 1972	. 2 |- ( A. z z = y -> F/ z [ y / x ] ph )
2		nfsb.1	. . 3 |- F/ z ph
3	2	nfsb4 2155	. 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 1403   F/wnf 1637   [wsb 1763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-nf 1638  df-sb 1764

This theorem is referenced by:  hbsb  2209  sb10f  2224  2sb8e  2235  sb8eu  2273  sb8euOLD  2274  2mo  2324  2moOLD  2325  2eu6OLD  2335  cbvabOLD  2544  cbvralf  3028  cbvreu  3032  cbvralsv  3045  cbvrexsv  3046  cbvrab  3057  cbvreucsf  3407  cbvrabcsf  3408  cbvopab1  4465  cbvmptf  4485  cbvmpt  4486  ralxpf  4970  cbviota  5538  sb8iota  5540  cbvriota  6250  dfoprab4f  6842  mo5f  27798  ax11-pm2  30973  2sb5nd  36357