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

Metamath Proof Explorer

Theorem rankeq0

Description: A set is empty iff its rank is empty. (Contributed by NM, 18-Sep-2006) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Hypothesis	rankeq0.1	$⊢ A \in V$
	Assertion	rankeq0	$⊢ A = \emptyset \leftrightarrow rank (A) = \emptyset$

Step	Hyp	Ref	Expression
1		rankeq0.1	$⊢ A \in V$
2		unir1	$⊢ ⋃ R_{1} [On] = V$
3	1 2	eleqtrri	$⊢ A \in ⋃ R_{1} [On]$
4		rankeq0b	$⊢ A \in ⋃ R_{1} [On] \to (A = \emptyset \leftrightarrow rank (A) = \emptyset)$
5	3 4	ax-mp	$⊢ A = \emptyset \leftrightarrow rank (A) = \emptyset$