Theorem elnelun

Description: The union of 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 yields the original set. (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	elnelun	$$⊢E\cup N=A$$

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	3	rabbii	$$⊢\left\{s\in A|B\notin C\right\}=\left\{s\in A|\neg B\in C\right\}$$
5	2 4	eqtri	$$⊢N=\left\{s\in A|\neg B\in C\right\}$$
6	1 5	uneq12i	$$⊢E\cup N=\left\{s\in A|B\in C\right\}\cup \left\{s\in A|\neg B\in C\right\}$$
7		rabxm	$$⊢A=\left\{s\in A|B\in C\right\}\cup \left\{s\in A|\neg B\in C\right\}$$
8	6 7	eqtr4i	$$⊢E\cup N=A$$