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 = { s e. A | B e. C }
	elneldisj.n	|- N = { s e. A | B e/ C }
Assertion	elnelun	|- ( E u. N ) = A

Proof

Step	Hyp	Ref	Expression
1		elneldisj.e	|- E = { s e. A | B e. C }
2		elneldisj.n	|- N = { s e. A | B e/ C }
3		df-nel	|- ( B e/ C <-> -. B e. C )
4	3	rabbii	|- { s e. A | B e/ C } = { s e. A | -. B e. C }
5	2 4	eqtri	|- N = { s e. A | -. B e. C }
6	1 5	uneq12i	|- ( E u. N ) = ( { s e. A | B e. C } u. { s e. A | -. B e. C } )
7		rabxm	|- A = ( { s e. A | B e. C } u. { s e. A | -. B e. C } )
8	6 7	eqtr4i	|- ( E u. N ) = A