Description: Bound-variable hypothesis builder for recs . (Contributed by Stefan O'Rear, 18-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nfrecs.f | ⊢ Ⅎ 𝑥 𝐹 | |
Assertion | nfrecs | ⊢ Ⅎ 𝑥 recs ( 𝐹 ) |
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 ( 𝐹 ) |