Theorem nfsb 1923

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 1919	. . 3 |- F/ z [ w / x ] ph
3	2	nfsbxy 1919	. 2 |- F/ z [ y / w ] [ w / x ] ph
4		ax-17 1503	. . . 4 |- ( ph -> A. w ph )
5	4	sbco2vh 1922	. . 3 |- ( [ y / w ] [ w / x ] ph <-> [ y / x ] ph )
6	5	nfbii 1450	. 2 |- ( F/ z [ y / w ] [ w / x ] ph <-> F/ z [ y / x ] ph )
7	3, 6	mpbi 144	1 |- F/ z [ y / x ] ph

Syntax hints:   F/wnf 1437   [wsb 1739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1740

This theorem is referenced by:  hbsb  1926  sbco2yz  1940  sbcomxyyz  1949  hbsbd  1959  nfsb4or  1998  sb8eu  2016  nfeu  2022  cbvab  2278  cbvralf  2671  cbvrexf  2672  cbvreu  2675  cbvralsv  2691  cbvrexsv  2692  cbvrab  2707  cbvreucsf  3091  cbvrabcsf  3092  cbvopab1  4033  cbvmptf  4054  cbvmpt  4055  ralxpf  4725  rexxpf  4726  cbviota  5133  sb8iota  5135  cbvriota  5780  dfoprab4f  6131