Theorem disjel

Description: A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015)

	Ref	Expression
Assertion	disjel	$$⊢\left(A\cap B=\varnothing \wedge C\in A\right)\to \neg C\in B$$

Proof

Step	Hyp	Ref	Expression
1		disj3	$$⊢A\cap B=\varnothing \leftrightarrow A=A\setminus B$$
2		eleq2	$$⊢A=A\setminus B\to \left(C\in A\leftrightarrow C\in \left(A\setminus B\right)\right)$$
3		eldifn	$$⊢C\in \left(A\setminus B\right)\to \neg C\in B$$
4	2 3	biimtrdi	$$⊢A=A\setminus B\to \left(C\in A\to \neg C\in B\right)$$
5	1 4	sylbi	$$⊢A\cap B=\varnothing \to \left(C\in A\to \neg C\in B\right)$$
6	5	imp	$$⊢\left(A\cap B=\varnothing \wedge C\in A\right)\to \neg C\in B$$