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
|- F/_ x F
Assertion nfrecs
|- F/_ x recs ( F )

Proof

Step Hyp Ref Expression
1 nfrecs.f
 |-  F/_ x F
2 df-recs
 |-  recs ( F ) = wrecs ( _E , On , F )
3 nfcv
 |-  F/_ x _E
4 nfcv
 |-  F/_ x On
5 3 4 1 nfwrecs
 |-  F/_ x wrecs ( _E , On , F )
6 2 5 nfcxfr
 |-  F/_ x recs ( F )