Description: The cumulative hierarchy of sets covers the universe. Proposition 4.45 (b) to (a) of Mendelson p. 281. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 8-Jun-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | unir1 | |- U. ( R1 " On ) = _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | setind | |- ( A. x ( x C_ U. ( R1 " On ) -> x e. U. ( R1 " On ) ) -> U. ( R1 " On ) = _V ) |
|
| 2 | vex | |- x e. _V |
|
| 3 | 2 | r1elss | |- ( x e. U. ( R1 " On ) <-> x C_ U. ( R1 " On ) ) |
| 4 | 3 | biimpri | |- ( x C_ U. ( R1 " On ) -> x e. U. ( R1 " On ) ) |
| 5 | 1 4 | mpg | |- U. ( R1 " On ) = _V |