nfwrd

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

		Ref	Expression
	Hypothesis	nfwrd.1	$⊢ \underline{Ⅎ} x S$
	Assertion	nfwrd	$⊢ \underline{Ⅎ} x Word S$

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

Metamath Proof Explorer