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 e. _V /\ C =/= B ) -> { A , B , C } = { A , B } )

Proof

Step Hyp Ref Expression
1 ianor 
 |-  ( -. ( C e. _V /\ C =/= B ) <-> ( -. C e. _V \/ -. C =/= B ) )
2 prprc2 
 |-  ( -. C e. _V -> { B , C } = { B } )
3 2 uneq1d 
 |-  ( -. C e. _V -> ( { B , C } u. { A } ) = ( { B } u. { A } ) )
4 tprot 
 |-  { A , B , C } = { B , C , A }
5 df-tp 
 |-  { B , C , A } = ( { B , C } u. { A } )
6 4 5 eqtri 
 |-  { A , B , C } = ( { B , C } u. { A } )
7 prcom 
 |-  { A , B } = { B , A }
8 df-pr 
 |-  { B , A } = ( { B } u. { A } )
9 7 8 eqtri 
 |-  { A , B } = ( { B } u. { A } )
10 3 6 9 3eqtr4g 
 |-  ( -. C e. _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 e. _V \/ -. C =/= B ) -> { A , B , C } = { A , B } )
16 1 15 sylbi 
 |-  ( -. ( C e. _V /\ C =/= B ) -> { A , B , C } = { A , B } )