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