Metamath Proof Explorer


Theorem prprc1

Description: A proper class vanishes in an unordered pair. (Contributed by NM, 15-Jul-1993)

Ref Expression
Assertion prprc1 ¬AVAB=B

Proof

Step Hyp Ref Expression
1 snprc ¬AVA=
2 uneq1 A=AB=B
3 df-pr AB=AB
4 uncom B=B
5 un0 B=B
6 4 5 eqtr2i B=B
7 2 3 6 3eqtr4g A=AB=B
8 1 7 sylbi ¬AVAB=B