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

Metamath Proof Explorer

Theorem rel0

Description: The empty set is a relation. (Contributed by NM, 26-Apr-1998)

		Ref	Expression
	Assertion	rel0	$⊢ Rel \emptyset$

Step	Hyp	Ref	Expression
1		0ss	$⊢ \emptyset \subseteq V \times V$
2		df-rel	$⊢ Rel \emptyset \leftrightarrow \emptyset \subseteq V \times V$
3	1 2	mpbir	$⊢ Rel \emptyset$