Theorem nfsb 2006

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

Syntax hints:  Ⅎwnf 1513  [wsb 1815

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816

This theorem is referenced by:  hbsb  2009  sbco2yz  2023  sbcomxyyz  2032  hbsbd  2042  nfsb4or  2081  sb8eu  2099  nfeu  2105  cbvab  2364  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvralsv  2802  cbvrexsv  2803  cbvrab  2819  cbvreucsf  3212  cbvrabcsf  3213  cbvopab1  4199  cbvmptf  4220  cbvmpt  4221  ralxpf  4921  rexxpf  4922  cbviota  5337  sb8iota  5340  cbvriota  6040  dfoprab4f  6417