Theorem nfwrd

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

	Ref	Expression
Hypothesis	nfwrd.1	|- F/_ x S
Assertion	nfwrd	|- F/_ x Word S

Proof

Step	Hyp	Ref	Expression
1		nfwrd.1	|- F/_ x S
2		df-word	|- Word S = { w | E. l e. NN0 w : ( 0 ..^ l ) --> S }
3		nfcv	|- F/_ x NN0
4		nfcv	|- F/_ x w
5		nfcv	|- F/_ x ( 0 ..^ l )
6	4 5 1	nff	|- F/ x w : ( 0 ..^ l ) --> S
7	3 6	nfrex	|- F/ x E. l e. NN0 w : ( 0 ..^ l ) --> S
8	7	nfab	|- F/_ x { w | E. l e. NN0 w : ( 0 ..^ l ) --> S }
9	2 8	nfcxfr	|- F/_ x Word S