nelun

Description: Negated membership for a union. (Contributed by Thierry Arnoux, 13-Dec-2023)

		Ref	Expression
	Assertion	nelun	$⊢ A = B \cup C \to (\neg X \in A \leftrightarrow (\neg X \in B \land \neg X \in C))$

Step	Hyp	Ref	Expression
1		eleq2	$⊢ A = B \cup C \to (X \in A \leftrightarrow X \in (B \cup C))$
2		elun	$⊢ X \in (B \cup C) \leftrightarrow (X \in B \lor X \in C)$
3	1 2	bitrdi	$⊢ A = B \cup C \to (X \in A \leftrightarrow (X \in B \lor X \in C))$
4	3	notbid	$⊢ A = B \cup C \to (\neg X \in A \leftrightarrow \neg (X \in B \lor X \in C))$
5		ioran	$⊢ \neg (X \in B \lor X \in C) \leftrightarrow (\neg X \in B \land \neg X \in C)$
6	4 5	bitrdi	$⊢ A = B \cup C \to (\neg X \in A \leftrightarrow (\neg X \in B \land \neg X \in C))$

Metamath Proof Explorer