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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ianor | |
|
2 | prprc2 | |
|
3 | 2 | uneq1d | |
4 | tprot | |
|
5 | df-tp | |
|
6 | 4 5 | eqtri | |
7 | prcom | |
|
8 | df-pr | |
|
9 | 7 8 | eqtri | |
10 | 3 6 9 | 3eqtr4g | |
11 | nne | |
|
12 | tppreq3 | |
|
13 | 12 | eqcoms | |
14 | 11 13 | sylbi | |
15 | 10 14 | jaoi | |
16 | 1 15 | sylbi | |