Theorem nprrel

Description: No proper class is related to anything via any relation. (Contributed by Roy F. Longton, 30-Jul-2005)

	Ref	Expression
Hypotheses	nprrel12.1	$$⊢\mathrm{Rel}R$$
	nprrel.2	$$⊢\neg A\in \mathrm{V}$$
Assertion	nprrel	$$⊢\neg ARB$$

Proof

Step	Hyp	Ref	Expression
1		nprrel12.1	$$⊢\mathrm{Rel}R$$
2		nprrel.2	$$⊢\neg A\in \mathrm{V}$$
3	1	brrelex1i	$$⊢ARB\to A\in \mathrm{V}$$
4	2 3	mto	$$⊢\neg ARB$$