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 𝑅
	nprrel.2	⊢ ¬ 𝐴 ∈ V
Assertion	nprrel	⊢ ¬ 𝐴 𝑅 𝐵

Proof

Step	Hyp	Ref	Expression
1		nprrel12.1	⊢ Rel 𝑅
2		nprrel.2	⊢ ¬ 𝐴 ∈ V
3	1	brrelex1i	⊢ ( 𝐴 𝑅 𝐵 → 𝐴 ∈ V )
4	2 3	mto	⊢ ¬ 𝐴 𝑅 𝐵