Metamath Proof Explorer


Theorem nprrel12

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

Ref Expression
Hypothesis nprrel12.1 RelR
Assertion nprrel12 ¬AVBV¬ARB

Proof

Step Hyp Ref Expression
1 nprrel12.1 RelR
2 1 brrelex12i ARBAVBV
3 2 con3i ¬AVBV¬ARB