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

Metamath Proof Explorer

Theorem nrelv

Description: The universal class is not a relation. (Contributed by Thierry Arnoux, 23-Jan-2022)

		Ref	Expression
	Assertion	nrelv	$⊢ \neg Rel V$

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		0nelxp	$⊢ \neg \emptyset \in (V \times V)$
3		nelss	$⊢ (\emptyset \in V \land \neg \emptyset \in (V \times V)) \to \neg V \subseteq V \times V$
4	1 2 3	mp2an	$⊢ \neg V \subseteq V \times V$
5		df-rel	$⊢ Rel V \leftrightarrow V \subseteq V \times V$
6	4 5	mtbir	$⊢ \neg Rel V$