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

Metamath Proof Explorer

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