Theorem nfsb 2006

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.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)

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

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfsb.1	. . . 4 |- F/ z ph
2	1	nfsbxy 2002	. . 3 |- F/ z [ w / x ] ph
3	2	nfsbxy 2002	. 2 |- F/ z [ y / w ] [ w / x ] ph
4		ax-17 1579	. . . 4 |- ( ph -> A. w ph )
5	4	sbco2vh 2005	. . 3 |- ( [ y / w ] [ w / x ] ph <-> [ y / x ] ph )
6	5	nfbii 1526	. 2 |- ( F/ z [ y / w ] [ w / x ] ph <-> F/ z [ y / x ] ph )
7	3, 6	mpbi 145	1 |- F/ z [ y / x ] ph

This proof depends on syntax axioms:   F/wnf 1513   [wsb 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816

This theorem is used by:  hbsb  2009  sbco2yz  2023  sbcomxyyz  2032  hbsbd  2042  nfsb4or  2081  sb8eu  2099  nfeu  2105  cbvab  2364  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvralsv  2802  cbvrexsv  2803  cbvrab  2819  cbvreucsf  3212  cbvrabcsf  3213  cbvopab1  4204  cbvmptf  4225  cbvmpt  4226  ralxpf  4926  rexxpf  4927  cbviota  5342  sb8iota  5345  cbvriota  6050  dfoprab4f  6427