This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ ⋃ R_{1} [On] = V$

Proof

Step	Hyp	Ref	Expression
1		setind	$⊢ \forall x (x \subseteq ⋃ R_{1} [On] \to x \in ⋃ R_{1} [On]) \to ⋃ R_{1} [On] = V$
2		vex	$⊢ x \in V$
3	2	r1elss	$⊢ x \in ⋃ R_{1} [On] \leftrightarrow x \subseteq ⋃ R_{1} [On]$
4	3	biimpri	$⊢ x \subseteq ⋃ R_{1} [On] \to x \in ⋃ R_{1} [On]$
5	1 4	mpg	$⊢ ⋃ R_{1} [On] = V$