Theorem disjprsn

Description: The disjoint intersection of an unordered pair and a singleton. (Contributed by AV, 23-Jan-2021)

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

Proof

Step	Hyp	Ref	Expression
1		dfsn2	$$⊢\left\{C\right\}=\left\{C,C\right\}$$
2	1	ineq2i	$$⊢\left\{A,B\right\}\cap \left\{C\right\}=\left\{A,B\right\}\cap \left\{C,C\right\}$$
3		disjpr2	$$⊢\left(\left(A\ne C\wedge B\ne C\right)\wedge \left(A\ne C\wedge B\ne C\right)\right)\to \left\{A,B\right\}\cap \left\{C,C\right\}=\varnothing$$
4	3	anidms	$$⊢\left(A\ne C\wedge B\ne C\right)\to \left\{A,B\right\}\cap \left\{C,C\right\}=\varnothing$$
5	2 4	syl5eq	$$⊢\left(A\ne C\wedge B\ne C\right)\to \left\{A,B\right\}\cap \left\{C\right\}=\varnothing$$