Description: The cumulative hierarchy of sets function is a function. (Contributed by Mario Carneiro, 16-Nov-2014) Extract this statement from its conjunction with r1dmlim . (Revised by BJ, 27-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r1fun | |- Fun R1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rdgfun | |- Fun rec ( ( x e. _V |-> ~P x ) , (/) ) |
|
| 2 | df-r1 | |- R1 = rec ( ( x e. _V |-> ~P x ) , (/) ) |
|
| 3 | 2 | funeqi | |- ( Fun R1 <-> Fun rec ( ( x e. _V |-> ~P x ) , (/) ) ) |
| 4 | 1 3 | mpbir | |- Fun R1 |