Theorem disjtpsn

Description: The disjoint intersection of an unordered triple and a singleton. (Contributed by AV, 14-Nov-2021)

	Ref	Expression
Assertion	disjtpsn	$$⊢\left(A\ne D\wedge B\ne D\wedge C\ne D\right)\to \left\{A,B,C\right\}\cap \left\{D\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-tp	$$⊢\left\{A,B,C\right\}=\left\{A,B\right\}\cup \left\{C\right\}$$
2	1	ineq1i	$$⊢\left\{A,B,C\right\}\cap \left\{D\right\}=\left(\left\{A,B\right\}\cup \left\{C\right\}\right)\cap \left\{D\right\}$$
3		disjprsn	$$⊢\left(A\ne D\wedge B\ne D\right)\to \left\{A,B\right\}\cap \left\{D\right\}=\varnothing$$
4	3	3adant3	$$⊢\left(A\ne D\wedge B\ne D\wedge C\ne D\right)\to \left\{A,B\right\}\cap \left\{D\right\}=\varnothing$$
5		disjsn2	$$⊢C\ne D\to \left\{C\right\}\cap \left\{D\right\}=\varnothing$$
6	5	3ad2ant3	$$⊢\left(A\ne D\wedge B\ne D\wedge C\ne D\right)\to \left\{C\right\}\cap \left\{D\right\}=\varnothing$$
7	4 6	jca	$$⊢\left(A\ne D\wedge B\ne D\wedge C\ne D\right)\to \left(\left\{A,B\right\}\cap \left\{D\right\}=\varnothing \wedge \left\{C\right\}\cap \left\{D\right\}=\varnothing \right)$$
8		undisj1	$$⊢\left(\left\{A,B\right\}\cap \left\{D\right\}=\varnothing \wedge \left\{C\right\}\cap \left\{D\right\}=\varnothing \right)\leftrightarrow \left(\left\{A,B\right\}\cup \left\{C\right\}\right)\cap \left\{D\right\}=\varnothing$$
9	7 8	sylib	$$⊢\left(A\ne D\wedge B\ne D\wedge C\ne D\right)\to \left(\left\{A,B\right\}\cup \left\{C\right\}\right)\cap \left\{D\right\}=\varnothing$$
10	2 9	syl5eq	$$⊢\left(A\ne D\wedge B\ne D\wedge C\ne D\right)\to \left\{A,B,C\right\}\cap \left\{D\right\}=\varnothing$$