Description: Value of the cumulative hierarchy of sets function at (/) . Part of Definition 9.9 of TakeutiZaring p. 76. (Contributed by NM, 2-Sep-2003) (Revised by Mario Carneiro, 10-Sep-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r10 | |- ( R1 ` (/) ) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-r1 | |- R1 = rec ( ( x e. _V |-> ~P x ) , (/) ) |
|
| 2 | 1 | fveq1i | |- ( R1 ` (/) ) = ( rec ( ( x e. _V |-> ~P x ) , (/) ) ` (/) ) |
| 3 | 0ex | |- (/) e. _V |
|
| 4 | 3 | rdg0 | |- ( rec ( ( x e. _V |-> ~P x ) , (/) ) ` (/) ) = (/) |
| 5 | 2 4 | eqtri | |- ( R1 ` (/) ) = (/) |