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	|- Rel R
	nprrel.2	|- -. A e. _V
Assertion	nprrel	|- -. A R B

Proof

Step	Hyp	Ref	Expression
1		nprrel12.1	|- Rel R
2		nprrel.2	|- -. A e. _V
3	1	brrelex1i	|- ( A R B -> A e. _V )
4	2 3	mto	|- -. A R B