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 |