rexdifsn

Description: Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015)

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

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ x \in (A ∖ \{B\}) \leftrightarrow (x \in A \land x \neq B)$
2	1	anbi1i	$⊢ (x \in (A ∖ \{B\}) \land φ) \leftrightarrow ((x \in A \land x \neq B) \land φ)$
3		anass	$⊢ ((x \in A \land x \neq B) \land φ) \leftrightarrow (x \in A \land (x \neq B \land φ))$
4	2 3	bitri	$⊢ (x \in (A ∖ \{B\}) \land φ) \leftrightarrow (x \in A \land (x \neq B \land φ))$
5	4	rexbii2	$⊢ \exists x \in (A ∖ \{B\}) φ \leftrightarrow \exists x \in A (x \neq B \land φ)$

Metamath Proof Explorer