Theorem disjne

Description: Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	disjne	$$⊢\left(A\cap B=\varnothing \wedge C\in A\wedge D\in B\right)\to C\ne D$$

Proof

Step	Hyp	Ref	Expression
1		disj	$$⊢A\cap B=\varnothing \leftrightarrow \forall x\in A\neg x\in B$$
2		eleq1	$$⊢x=C\to \left(x\in B\leftrightarrow C\in B\right)$$
3	2	notbid	$$⊢x=C\to \left(\neg x\in B\leftrightarrow \neg C\in B\right)$$
4	3	rspccva	$$⊢\left(\forall x\in A\neg x\in B\wedge C\in A\right)\to \neg C\in B$$
5		eleq1a	$$⊢D\in B\to \left(C=D\to C\in B\right)$$
6	5	necon3bd	$$⊢D\in B\to \left(\neg C\in B\to C\ne D\right)$$
7	4 6	syl5com	$$⊢\left(\forall x\in A\neg x\in B\wedge C\in A\right)\to \left(D\in B\to C\ne D\right)$$
8	1 7	sylanb	$$⊢\left(A\cap B=\varnothing \wedge C\in A\right)\to \left(D\in B\to C\ne D\right)$$
9	8	3impia	$$⊢\left(A\cap B=\varnothing \wedge C\in A\wedge D\in B\right)\to C\ne D$$