This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rexdifpr

Description: Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018) (Proof shortened by Wolf Lammen, 15-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		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 φ))$
2		eldifpr	$⊢ x \in (A ∖ \{B, C\}) \leftrightarrow (x \in A \land x \neq B \land x \neq C)$
3		3anass	$⊢ (x \in A \land x \neq B \land x \neq C) \leftrightarrow (x \in A \land (x \neq B \land x \neq C))$
4	2 3	bitri	$⊢ x \in (A ∖ \{B, C\}) \leftrightarrow (x \in A \land (x \neq B \land x \neq C))$
5	4	anbi1i	$⊢ (x \in (A ∖ \{B, 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	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 φ))$
8	1 5 7	3bitr4i	$⊢ (x \in (A ∖ \{B, C\}) \land φ) \leftrightarrow (x \in A \land (x \neq B \land x \neq C \land φ))$
9	8	rexbii2	$⊢ \exists x \in (A ∖ \{B, C\}) φ \leftrightarrow \exists x \in A (x \neq B \land x \neq C \land φ)$