Metamath Proof Explorer


Theorem unir1

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

Proof

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