Metamath Proof Explorer


Theorem prprc2

Description: A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006)

Ref Expression
Assertion prprc2 ¬BVAB=A

Proof

Step Hyp Ref Expression
1 prcom AB=BA
2 prprc1 ¬BVBA=A
3 1 2 eqtrid ¬BVAB=A