inpr0

Description: Rewrite an empty intersection with a pair. (Contributed by Thierry Arnoux, 20-Nov-2023)

		Ref	Expression
	Assertion	inpr0	$⊢ A \cap \{B, C\} = \emptyset \leftrightarrow (\neg B \in A \land \neg C \in A)$

Step	Hyp	Ref	Expression
1		r19.26	$⊢ \forall x \in A (x \neq B \land x \neq C) \leftrightarrow (\forall x \in A x \neq B \land \forall x \in A x \neq C)$
2		nelpr	$⊢ x \in V \to (\neg x \in \{B, C\} \leftrightarrow (x \neq B \land x \neq C))$
3	2	elv	$⊢ \neg x \in \{B, C\} \leftrightarrow (x \neq B \land x \neq C)$
4	3	imbi2i	$⊢ (x \in A \to \neg x \in \{B, C\}) \leftrightarrow (x \in A \to (x \neq B \land x \neq C))$
5	4	albii	$⊢ \forall x (x \in A \to \neg x \in \{B, C\}) \leftrightarrow \forall x (x \in A \to (x \neq B \land x \neq C))$
6		disj1	$⊢ A \cap \{B, C\} = \emptyset \leftrightarrow \forall x (x \in A \to \neg x \in \{B, C\})$
7		df-ral	$⊢ \forall x \in A (x \neq B \land x \neq C) \leftrightarrow \forall x (x \in A \to (x \neq B \land x \neq C))$
8	5 6 7	3bitr4i	$⊢ A \cap \{B, C\} = \emptyset \leftrightarrow \forall x \in A (x \neq B \land x \neq C)$
9		nelb	$⊢ \neg B \in A \leftrightarrow \forall x \in A x \neq B$
10		nelb	$⊢ \neg C \in A \leftrightarrow \forall x \in A x \neq C$
11	9 10	anbi12i	$⊢ (\neg B \in A \land \neg C \in A) \leftrightarrow (\forall x \in A x \neq B \land \forall x \in A x \neq C)$
12	1 8 11	3bitr4i	$⊢ A \cap \{B, C\} = \emptyset \leftrightarrow (\neg B \in A \land \neg C \in A)$

Metamath Proof Explorer