Theorem nfwrd

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

	Ref	Expression
Hypothesis	nfwrd.1	⊢ Ⅎ 𝑥 𝑆
Assertion	nfwrd	⊢ Ⅎ 𝑥 Word 𝑆

Proof

Step	Hyp	Ref	Expression
1		nfwrd.1	⊢ Ⅎ 𝑥 𝑆
2		df-word	⊢ Word 𝑆 = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 }
3		nfcv	⊢ Ⅎ 𝑥 ℕ0
4		nfcv	⊢ Ⅎ 𝑥 𝑤
5		nfcv	⊢ Ⅎ 𝑥 ( 0 ..^ 𝑙 )
6	4 5 1	nff	⊢ Ⅎ 𝑥 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆
7	3 6	nfrexw	⊢ Ⅎ 𝑥 ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆
8	7	nfab	⊢ Ⅎ 𝑥 { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 }
9	2 8	nfcxfr	⊢ Ⅎ 𝑥 Word 𝑆