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 ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐵 ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )

Proof

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