This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ¬ C ∈ V ∧ C ≠ B → A B C = A B

Proof

Step Hyp Ref Expression
1 ianor ⊢ ¬ C ∈ V ∧ C ≠ B ↔ ¬ C ∈ V ∨ ¬ C ≠ B
2 prprc2 ⊢ ¬ C ∈ V → B C = B
3 2 uneq1d ⊢ ¬ C ∈ V → B C ∪ A = B ∪ A
4 tprot ⊢ A B C = B C A
5 df-tp ⊢ B C A = B C ∪ A
6 4 5 eqtri ⊢ A B C = B C ∪ A
7 prcom ⊢ A B = B A
8 df-pr ⊢ B A = B ∪ A
9 7 8 eqtri ⊢ A B = B ∪ A
10 3 6 9 3eqtr4g ⊢ ¬ C ∈ V → A B C = A B
11 nne ⊢ ¬ C ≠ B ↔ C = B
12 tppreq3 ⊢ B = C → A B C = A B
13 12 eqcoms ⊢ C = B → A B C = A B
14 11 13 sylbi ⊢ ¬ C ≠ B → A B C = A B
15 10 14 jaoi ⊢ ¬ C ∈ V ∨ ¬ C ≠ B → A B C = A B
16 1 15 sylbi ⊢ ¬ C ∈ V ∧ C ≠ B → A B C = A B