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 \in A \| B \in C\}$
	elneldisj.n	$⊢ N = \{s \in A \| B \notin C\}$
Assertion	elneldisj	$⊢ E \cap N = \emptyset$

Proof

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

Metamath Proof Explorer

Theorem elneldisj

Proof