Theorem nprrel12

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

	Ref	Expression
Hypothesis	nprrel12.1	$$⊢\mathrm{Rel}R$$
Assertion	nprrel12	$$⊢\neg \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \neg ARB$$

Proof

Step	Hyp	Ref	Expression
1		nprrel12.1	$$⊢\mathrm{Rel}R$$
2	1	brrelex12i	$$⊢ARB\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
3	2	con3i	$$⊢\neg \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \neg ARB$$