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

Metamath Proof Explorer

Theorem r1val2

Description: The value of the cumulative hierarchy of sets function expressed in terms of rank. Definition 15.19 of Monk1 p. 113. (Contributed by NM, 30-Nov-2003)

		Ref	Expression
	Assertion	r1val2	$⊢ A \in On \to R_{1} (A) = \{x \| rank (x) \in A\}$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2	1	rankr1a	$⊢ A \in On \to (x \in R_{1} (A) \leftrightarrow rank (x) \in A)$
3	2	eqabdv	$⊢ A \in On \to R_{1} (A) = \{x \| rank (x) \in A\}$