Metamath Proof Explorer


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 ( 𝐹 )