Theorem nfsb 1999

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

Syntax hints:  Ⅎwnf 1509  [wsb 1810

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 1811

This theorem is referenced by:  hbsb  2002  sbco2yz  2016  sbcomxyyz  2025  hbsbd  2035  nfsb4or  2074  sb8eu  2092  nfeu  2098  cbvab  2356  cbvralf  2759  cbvrexf  2760  cbvreu  2766  cbvralsv  2784  cbvrexsv  2785  cbvrab  2801  cbvreucsf  3193  cbvrabcsf  3194  cbvopab1  4167  cbvmptf  4188  cbvmpt  4189  ralxpf  4882  rexxpf  4883  cbviota  5298  sb8iota  5301  cbvriota  5993  dfoprab4f  6365