Theorem elneldisj

Description: The set of elements s determining classes C (which may depend on s ) containing a special element and the set of elements s determining classes C not containing the special element are disjoint. (Contributed by Alexander van der Vekens, 11-Jan-2018) (Revised by AV, 9-Nov-2020) (Revised by AV, 17-Dec-2021)

	Ref	Expression
Hypotheses	elneldisj.e	$$⊢E=\left\{s\in A|B\in C\right\}$$
	elneldisj.n	$$⊢N=\left\{s\in A|B\notin C\right\}$$
Assertion	elneldisj	$$⊢E\cap N=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		elneldisj.e	$$⊢E=\left\{s\in A|B\in C\right\}$$
2		elneldisj.n	$$⊢N=\left\{s\in A|B\notin C\right\}$$
3		df-nel	$$⊢B\notin C\leftrightarrow \neg B\in C$$
4	2 3	rabbieq	$$⊢N=\left\{s\in A|\neg B\in C\right\}$$
5	1 4	ineq12i	$$⊢E\cap N=\left\{s\in A|B\in C\right\}\cap \left\{s\in A|\neg B\in C\right\}$$
6		rabnc	$$⊢\left\{s\in A|B\in C\right\}\cap \left\{s\in A|\neg B\in C\right\}=\varnothing$$
7	5 6	eqtri	$$⊢E\cap N=\varnothing$$