Theorem diftpsn3

Description: Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017) (Proof shortened by JJ, 23-Jul-2021)

	Ref	Expression
Assertion	diftpsn3	|- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )

Proof

Step	Hyp	Ref	Expression
1		disjprsn	|- ( ( A =/= C /\ B =/= C ) -> ( { A , B } i^i { C } ) = (/) )
2		disj3	|- ( ( { A , B } i^i { C } ) = (/) <-> { A , B } = ( { A , B } \ { C } ) )
3	1 2	sylib	|- ( ( A =/= C /\ B =/= C ) -> { A , B } = ( { A , B } \ { C } ) )
4	3	eqcomd	|- ( ( A =/= C /\ B =/= C ) -> ( { A , B } \ { C } ) = { A , B } )
5		difid	|- ( { C } \ { C } ) = (/)
6	5	a1i	|- ( ( A =/= C /\ B =/= C ) -> ( { C } \ { C } ) = (/) )
7	4 6	uneq12d	|- ( ( A =/= C /\ B =/= C ) -> ( ( { A , B } \ { C } ) u. ( { C } \ { C } ) ) = ( { A , B } u. (/) ) )
8		df-tp	|- { A , B , C } = ( { A , B } u. { C } )
9	8	difeq1i	|- ( { A , B , C } \ { C } ) = ( ( { A , B } u. { C } ) \ { C } )
10		difundir	|- ( ( { A , B } u. { C } ) \ { C } ) = ( ( { A , B } \ { C } ) u. ( { C } \ { C } ) )
11	9 10	eqtr2i	|- ( ( { A , B } \ { C } ) u. ( { C } \ { C } ) ) = ( { A , B , C } \ { C } )
12		un0	|- ( { A , B } u. (/) ) = { A , B }
13	7 11 12	3eqtr3g	|- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )