# Metamath Proof Explorer

## 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)↔\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$