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 \leftrightarrow \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\}$$