Metamath Proof Explorer


Theorem tpprceq3

Description: An unordered triple is an unordered pair if one of its elements is a proper class or is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017)

Ref Expression
Assertion tpprceq3 ¬CVCBABC=AB

Proof

Step Hyp Ref Expression
1 ianor ¬CVCB¬CV¬CB
2 prprc2 ¬CVBC=B
3 2 uneq1d ¬CVBCA=BA
4 tprot ABC=BCA
5 df-tp BCA=BCA
6 4 5 eqtri ABC=BCA
7 prcom AB=BA
8 df-pr BA=BA
9 7 8 eqtri AB=BA
10 3 6 9 3eqtr4g ¬CVABC=AB
11 nne ¬CBC=B
12 tppreq3 B=CABC=AB
13 12 eqcoms C=BABC=AB
14 11 13 sylbi ¬CBABC=AB
15 10 14 jaoi ¬CV¬CBABC=AB
16 1 15 sylbi ¬CVCBABC=AB