rexdifpr

Description: Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018)

		Ref	Expression
	Assertion	rexdifpr	$⊢ \exists x \in (A ∖ \{B, C\}) φ \leftrightarrow \exists x \in A (x \neq B \land x \neq C \land φ)$

Step	Hyp	Ref	Expression
1		eldifpr	$⊢ x \in (A ∖ \{B, C\}) \leftrightarrow (x \in A \land x \neq B \land x \neq C)$
2		3anass	$⊢ (x \in A \land x \neq B \land x \neq C) \leftrightarrow (x \in A \land (x \neq B \land x \neq C))$
3	1 2	bitri	$⊢ x \in (A ∖ \{B, C\}) \leftrightarrow (x \in A \land (x \neq B \land x \neq C))$
4	3	anbi1i	$⊢ (x \in (A ∖ \{B, C\}) \land φ) \leftrightarrow ((x \in A \land (x \neq B \land x \neq C)) \land φ)$
5		anass	$⊢ ((x \in A \land (x \neq B \land x \neq C)) \land φ) \leftrightarrow (x \in A \land ((x \neq B \land x \neq C) \land φ))$
6		df-3an	$⊢ (x \neq B \land x \neq C \land φ) \leftrightarrow ((x \neq B \land x \neq C) \land φ)$
7	6	bicomi	$⊢ ((x \neq B \land x \neq C) \land φ) \leftrightarrow (x \neq B \land x \neq C \land φ)$
8	7	anbi2i	$⊢ (x \in A \land ((x \neq B \land x \neq C) \land φ)) \leftrightarrow (x \in A \land (x \neq B \land x \neq C \land φ))$
9	5 8	bitri	$⊢ ((x \in A \land (x \neq B \land x \neq C)) \land φ) \leftrightarrow (x \in A \land (x \neq B \land x \neq C \land φ))$
10	4 9	bitri	$⊢ (x \in (A ∖ \{B, C\}) \land φ) \leftrightarrow (x \in A \land (x \neq B \land x \neq C \land φ))$
11	10	rexbii2	$⊢ \exists x \in (A ∖ \{B, C\}) φ \leftrightarrow \exists x \in A (x \neq B \land x \neq C \land φ)$

Metamath Proof Explorer