Theorem nfsb 1965

Description: If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)

Hypothesis

Ref	Expression
nfsb.1	⊢ Ⅎ𝑧𝜑

Assertion

Ref	Expression
nfsb	⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Distinct variable group:   𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem nfsb

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfsb.1	. . . 4 ⊢ Ⅎ𝑧𝜑
2	1	nfsbxy 1961	. . 3 ⊢ Ⅎ𝑧[𝑤 / 𝑥]𝜑
3	2	nfsbxy 1961	. 2 ⊢ Ⅎ𝑧[𝑦 / 𝑤][𝑤 / 𝑥]𝜑
4		ax-17 1540	. . . 4 ⊢ (𝜑 → ∀𝑤𝜑)
5	4	sbco2vh 1964	. . 3 ⊢ ([𝑦 / 𝑤][𝑤 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
6	5	nfbii 1487	. 2 ⊢ (Ⅎ𝑧[𝑦 / 𝑤][𝑤 / 𝑥]𝜑 ↔ Ⅎ𝑧[𝑦 / 𝑥]𝜑)
7	3, 6	mpbi 145	1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1474  [wsb 1776

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777

This theorem is referenced by:  hbsb  1968  sbco2yz  1982  sbcomxyyz  1991  hbsbd  2001  nfsb4or  2040  sb8eu  2058  nfeu  2064  cbvab  2320  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvralsv  2745  cbvrexsv  2746  cbvrab  2761  cbvreucsf  3149  cbvrabcsf  3150  cbvopab1  4106  cbvmptf  4127  cbvmpt  4128  ralxpf  4812  rexxpf  4813  cbviota  5224  sb8iota  5226  cbvriota  5888  dfoprab4f  6251