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

Metamath Proof Explorer

Theorem nprrel12

Description: Proper classes are not related via any relation. (Contributed by AV, 29-Oct-2021)

		Ref	Expression
	Hypothesis	nprrel12.1	$⊢ Rel R$
	Assertion	nprrel12	$⊢ \neg (A \in V \land B \in V) \to \neg A R B$

Step	Hyp	Ref	Expression
1		nprrel12.1	$⊢ Rel R$
2	1	brrelex12i	$⊢ A R B \to (A \in V \land B \in V)$
3	2	con3i	$⊢ \neg (A \in V \land B \in V) \to \neg A R B$