Theorem nfsb 1974

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 1970	. . 3 |- F/ z [ w / x ] ph
3	2	nfsbxy 1970	. 2 |- F/ z [ y / w ] [ w / x ] ph
4		ax-17 1549	. . . 4 |- ( ph -> A. w ph )
5	4	sbco2vh 1973	. . 3 |- ( [ y / w ] [ w / x ] ph <-> [ y / x ] ph )
6	5	nfbii 1496	. 2 |- ( F/ z [ y / w ] [ w / x ] ph <-> F/ z [ y / x ] ph )
7	3, 6	mpbi 145	1 |- F/ z [ y / x ] ph

Syntax hints:   F/wnf 1483   [wsb 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786

This theorem is referenced by:  hbsb  1977  sbco2yz  1991  sbcomxyyz  2000  hbsbd  2010  nfsb4or  2049  sb8eu  2067  nfeu  2073  cbvab  2329  cbvralf  2730  cbvrexf  2731  cbvreu  2736  cbvralsv  2754  cbvrexsv  2755  cbvrab  2770  cbvreucsf  3158  cbvrabcsf  3159  cbvopab1  4117  cbvmptf  4138  cbvmpt  4139  ralxpf  4824  rexxpf  4825  cbviota  5237  sb8iota  5239  cbvriota  5910  dfoprab4f  6279