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 } )