Metamath Proof Explorer

Theorem tppreqb

Description: An unordered triple is an unordered pair if and only if one of its elements is a proper class or is identical with one of the another elements. (Contributed by Alexander van der Vekens, 15-Jan-2018)

Ref Expression
Assertion tppreqb ⊢ ¬ C ∈ V ∧ C ≠ A ∧ C ≠ B ↔ A B C = A B

Proof

Step Hyp Ref Expression
1 3ianor ⊢ ¬ C ∈ V ∧ C ≠ A ∧ C ≠ B ↔ ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
2 df-3or ⊢ ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B ↔ ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
3 1 2 bitri ⊢ ¬ C ∈ V ∧ C ≠ A ∧ C ≠ B ↔ ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
4 orass ⊢ ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B ∨ ¬ C ∈ V ↔ ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B ∨ ¬ C ∈ V
5 ianor ⊢ ¬ C ∈ V ∧ C ≠ A ↔ ¬ C ∈ V ∨ ¬ C ≠ A
6 tpprceq3 ⊢ ¬ C ∈ V ∧ C ≠ A → B A C = B A
7 5 6 sylbir ⊢ ¬ C ∈ V ∨ ¬ C ≠ A → B A C = B A
8 tpcoma ⊢ B A C = A B C
9 prcom ⊢ B A = A B
10 7 8 9 3eqtr3g ⊢ ¬ C ∈ V ∨ ¬ C ≠ A → A B C = A B
11 orcom ⊢ ¬ C ≠ B ∨ ¬ C ∈ V ↔ ¬ C ∈ V ∨ ¬ C ≠ B
12 ianor ⊢ ¬ C ∈ V ∧ C ≠ B ↔ ¬ C ∈ V ∨ ¬ C ≠ B
13 11 12 bitr4i ⊢ ¬ C ≠ B ∨ ¬ C ∈ V ↔ ¬ C ∈ V ∧ C ≠ B
14 tpprceq3 ⊢ ¬ C ∈ V ∧ C ≠ B → A B C = A B
15 13 14 sylbi ⊢ ¬ C ≠ B ∨ ¬ C ∈ V → A B C = A B
16 10 15 jaoi ⊢ ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B ∨ ¬ C ∈ V → A B C = A B
17 4 16 sylbi ⊢ ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B ∨ ¬ C ∈ V → A B C = A B
18 17 orcs ⊢ ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B → A B C = A B
19 3 18 sylbi ⊢ ¬ C ∈ V ∧ C ≠ A ∧ C ≠ B → A B C = A B
20 df-tp ⊢ A B C = A B ∪ C
21 20 eqeq1i ⊢ A B C = A B ↔ A B ∪ C = A B
22 ssequn2 ⊢ C ⊆ A B ↔ A B ∪ C = A B
23 snssg ⊢ C ∈ V → C ∈ A B ↔ C ⊆ A B
24 elpri ⊢ C ∈ A B → C = A ∨ C = B
25 nne ⊢ ¬ C ≠ A ↔ C = A
26 3mix2 ⊢ ¬ C ≠ A → ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
27 25 26 sylbir ⊢ C = A → ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
28 nne ⊢ ¬ C ≠ B ↔ C = B
29 3mix3 ⊢ ¬ C ≠ B → ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
30 28 29 sylbir ⊢ C = B → ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
31 27 30 jaoi ⊢ C = A ∨ C = B → ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
32 24 31 syl ⊢ C ∈ A B → ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
33 23 32 syl6bir ⊢ C ∈ V → C ⊆ A B → ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
34 3mix1 ⊢ ¬ C ∈ V → ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
35 34 a1d ⊢ ¬ C ∈ V → C ⊆ A B → ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
36 33 35 pm2.61i ⊢ C ⊆ A B → ¬ C ∈ V ∨ ¬ C ≠ A ∨ ¬ C ≠ B
37 36 1 sylibr ⊢ C ⊆ A B → ¬ C ∈ V ∧ C ≠ A ∧ C ≠ B
38 22 37 sylbir ⊢ A B ∪ C = A B → ¬ C ∈ V ∧ C ≠ A ∧ C ≠ B
39 21 38 sylbi ⊢ A B C = A B → ¬ C ∈ V ∧ C ≠ A ∧ C ≠ B
40 19 39 impbii ⊢ ¬ C ∈ V ∧ C ≠ A ∧ C ≠ B ↔ A B C = A B