# 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 ${⊢}\left({A}\ne {C}\wedge {B}\ne {C}\right)\to \left\{{A},{B},{C}\right\}\setminus \left\{{C}\right\}=\left\{{A},{B}\right\}$

### Proof

Step Hyp Ref Expression
1 disjprsn ${⊢}\left({A}\ne {C}\wedge {B}\ne {C}\right)\to \left\{{A},{B}\right\}\cap \left\{{C}\right\}=\varnothing$
2 disj3 ${⊢}\left\{{A},{B}\right\}\cap \left\{{C}\right\}=\varnothing ↔\left\{{A},{B}\right\}=\left\{{A},{B}\right\}\setminus \left\{{C}\right\}$
3 1 2 sylib ${⊢}\left({A}\ne {C}\wedge {B}\ne {C}\right)\to \left\{{A},{B}\right\}=\left\{{A},{B}\right\}\setminus \left\{{C}\right\}$
4 3 eqcomd ${⊢}\left({A}\ne {C}\wedge {B}\ne {C}\right)\to \left\{{A},{B}\right\}\setminus \left\{{C}\right\}=\left\{{A},{B}\right\}$
5 difid ${⊢}\left\{{C}\right\}\setminus \left\{{C}\right\}=\varnothing$
6 5 a1i ${⊢}\left({A}\ne {C}\wedge {B}\ne {C}\right)\to \left\{{C}\right\}\setminus \left\{{C}\right\}=\varnothing$
7 4 6 uneq12d ${⊢}\left({A}\ne {C}\wedge {B}\ne {C}\right)\to \left(\left\{{A},{B}\right\}\setminus \left\{{C}\right\}\right)\cup \left(\left\{{C}\right\}\setminus \left\{{C}\right\}\right)=\left\{{A},{B}\right\}\cup \varnothing$
8 df-tp ${⊢}\left\{{A},{B},{C}\right\}=\left\{{A},{B}\right\}\cup \left\{{C}\right\}$
9 8 difeq1i ${⊢}\left\{{A},{B},{C}\right\}\setminus \left\{{C}\right\}=\left(\left\{{A},{B}\right\}\cup \left\{{C}\right\}\right)\setminus \left\{{C}\right\}$
10 difundir ${⊢}\left(\left\{{A},{B}\right\}\cup \left\{{C}\right\}\right)\setminus \left\{{C}\right\}=\left(\left\{{A},{B}\right\}\setminus \left\{{C}\right\}\right)\cup \left(\left\{{C}\right\}\setminus \left\{{C}\right\}\right)$
11 9 10 eqtr2i ${⊢}\left(\left\{{A},{B}\right\}\setminus \left\{{C}\right\}\right)\cup \left(\left\{{C}\right\}\setminus \left\{{C}\right\}\right)=\left\{{A},{B},{C}\right\}\setminus \left\{{C}\right\}$
12 un0 ${⊢}\left\{{A},{B}\right\}\cup \varnothing =\left\{{A},{B}\right\}$
13 7 11 12 3eqtr3g ${⊢}\left({A}\ne {C}\wedge {B}\ne {C}\right)\to \left\{{A},{B},{C}\right\}\setminus \left\{{C}\right\}=\left\{{A},{B}\right\}$