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

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	ineq12i	|- ( E i^i N ) = ( { s e. A | B e. C } i^i { s e. A | -. B e. C } )
7		rabnc	|- ( { s e. A | B e. C } i^i { s e. A | -. B e. C } ) = (/)
8	6 7	eqtri	|- ( E i^i N ) = (/)