Description: The cumulative hierarchy of sets function is a function on the class of ordinal numbers. (Contributed by NM, 5-Oct-2003) (Revised by Mario Carneiro, 10-Sep-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r1fnon | |- R1 Fn On |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rdgfnon | |- rec ( ( x e. _V |-> ~P x ) , (/) ) Fn On |
|
| 2 | df-r1 | |- R1 = rec ( ( x e. _V |-> ~P x ) , (/) ) |
|
| 3 | 2 | fneq1i | |- ( R1 Fn On <-> rec ( ( x e. _V |-> ~P x ) , (/) ) Fn On ) |
| 4 | 1 3 | mpbir | |- R1 Fn On |