Theorem nfrecs

Description: Bound-variable hypothesis builder for recs . (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypothesis	nfrecs.f	⊢ Ⅎ 𝑥 𝐹
Assertion	nfrecs	⊢ Ⅎ 𝑥 recs ( 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		nfrecs.f	⊢ Ⅎ 𝑥 𝐹
2		df-recs	⊢ recs ( 𝐹 ) = wrecs ( E , On , 𝐹 )
3		nfcv	⊢ Ⅎ 𝑥 E
4		nfcv	⊢ Ⅎ 𝑥 On
5	3 4 1	nfwrecs	⊢ Ⅎ 𝑥 wrecs ( E , On , 𝐹 )
6	2 5	nfcxfr	⊢ Ⅎ 𝑥 recs ( 𝐹 )