Theorem nfsb 2236

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 2001	. 2 |- ( A. z z = y -> F/ z [ y / x ] ph )
2		nfsb.1	. . 3 |- F/ z ph
3	2	nfsb4 2185	. 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 1436   F/wnf 1664   [wsb 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1661  df-nf 1665  df-sb 1788

This theorem is referenced by:  hbsb  2237  sb10f  2252  2sb8e  2263  sb8eu  2300  2mo  2348  2moOLD  2349  cbvabOLD  2565  cbvralf  3050  cbvreu  3054  cbvralsv  3067  cbvrexsv  3068  cbvrab  3080  cbvreucsf  3430  cbvrabcsf  3431  cbvopab1  4492  cbvmptf  4512  cbvmpt  4513  ralxpf  4998  cbviota  5568  sb8iota  5570  cbvriota  6275  dfoprab4f  6863  mo5f  28112  ax11-pm2  31402  2sb5nd  36829