Theorem nfsb 1944

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 1940	. . 3 |- F/ z [ w / x ] ph
3	2	nfsbxy 1940	. 2 |- F/ z [ y / w ] [ w / x ] ph
4		ax-17 1524	. . . 4 |- ( ph -> A. w ph )
5	4	sbco2vh 1943	. . 3 |- ( [ y / w ] [ w / x ] ph <-> [ y / x ] ph )
6	5	nfbii 1471	. 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 1458   [wsb 1760

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761

This theorem is referenced by:  hbsb  1947  sbco2yz  1961  sbcomxyyz  1970  hbsbd  1980  nfsb4or  2019  sb8eu  2037  nfeu  2043  cbvab  2299  cbvralf  2694  cbvrexf  2695  cbvreu  2699  cbvralsv  2717  cbvrexsv  2718  cbvrab  2733  cbvreucsf  3119  cbvrabcsf  3120  cbvopab1  4071  cbvmptf  4092  cbvmpt  4093  ralxpf  4766  rexxpf  4767  cbviota  5175  sb8iota  5177  cbvriota  5831  dfoprab4f  6184