Theorem nfwrd

Description: Hypothesis builder for Word S . (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Hypothesis	nfwrd.1	$$⊢\underset{\_}{Ⅎ}xS$$
Assertion	nfwrd	$$⊢\underset{\_}{Ⅎ}x\mathrm{Word}S$$

Proof

Step	Hyp	Ref	Expression
1		nfwrd.1	$$⊢\underset{\_}{Ⅎ}xS$$
2		df-word	$$⊢\mathrm{Word}S=\left\{w|\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶S\right\}$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}x{\mathbb{N}}_0$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}x\left(0..^l\right)$$
6	4 5 1	nff	$$⊢Ⅎxw:\left(0..^l\right)⟶S$$
7	3 6	nfrexw	$$⊢Ⅎx\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶S$$
8	7	nfab	$$⊢\underset{\_}{Ⅎ}x\left\{w|\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶S\right\}$$
9	2 8	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\mathrm{Word}S$$