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 ( 𝑅1 “ On ) = V

Proof

Step Hyp Ref Expression
1 setind ( ∀ 𝑥 ( 𝑥 ( 𝑅1 “ On ) → 𝑥 ( 𝑅1 “ On ) ) → ( 𝑅1 “ On ) = V )
2 vex 𝑥 ∈ V
3 2 r1elss ( 𝑥 ( 𝑅1 “ On ) ↔ 𝑥 ( 𝑅1 “ On ) )
4 3 biimpri ( 𝑥 ( 𝑅1 “ On ) → 𝑥 ( 𝑅1 “ On ) )
5 1 4 mpg ( 𝑅1 “ On ) = V