Theorem nprrel12

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

	Ref	Expression
Hypothesis	nprrel12.1	⊢ Rel 𝑅
Assertion	nprrel12	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ¬ 𝐴 𝑅 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nprrel12.1	⊢ Rel 𝑅
2	1	brrelex12i	⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
3	2	con3i	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ¬ 𝐴 𝑅 𝐵 )