Theorem nfsb 2000

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 1996	. . 3 ⊢ Ⅎ𝑧[𝑤 / 𝑥]𝜑
3	2	nfsbxy 1996	. 2 ⊢ Ⅎ𝑧[𝑦 / 𝑤][𝑤 / 𝑥]𝜑
4		ax-17 1575	. . . 4 ⊢ (𝜑 → ∀𝑤𝜑)
5	4	sbco2vh 1999	. . 3 ⊢ ([𝑦 / 𝑤][𝑤 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
6	5	nfbii 1522	. 2 ⊢ (Ⅎ𝑧[𝑦 / 𝑤][𝑤 / 𝑥]𝜑 ↔ Ⅎ𝑧[𝑦 / 𝑥]𝜑)
7	3, 6	mpbi 145	1 ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1509  [wsb 1811

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812

This theorem is referenced by:  hbsb  2003  sbco2yz  2017  sbcomxyyz  2026  hbsbd  2036  nfsb4or  2075  sb8eu  2093  nfeu  2099  cbvab  2358  cbvralf  2769  cbvrexf  2770  cbvreu  2776  cbvralsv  2794  cbvrexsv  2795  cbvrab  2811  cbvreucsf  3203  cbvrabcsf  3204  cbvopab1  4183  cbvmptf  4204  cbvmpt  4205  ralxpf  4901  rexxpf  4902  cbviota  5317  sb8iota  5320  cbvriota  6015  dfoprab4f  6387