raldifsni

Description: Rearrangement of a property of a singleton difference. (Contributed by Stefan O'Rear, 27-Feb-2015)

		Ref	Expression
	Assertion	raldifsni	$⊢ \forall x \in (A ∖ \{B\}) \neg φ \leftrightarrow \forall x \in A (φ \to x = B)$

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ x \in (A ∖ \{B\}) \leftrightarrow (x \in A \land x \neq B)$
2	1	imbi1i	$⊢ (x \in (A ∖ \{B\}) \to \neg φ) \leftrightarrow ((x \in A \land x \neq B) \to \neg φ)$
3		impexp	$⊢ ((x \in A \land x \neq B) \to \neg φ) \leftrightarrow (x \in A \to (x \neq B \to \neg φ))$
4		df-ne	$⊢ x \neq B \leftrightarrow \neg x = B$
5	4	imbi1i	$⊢ (x \neq B \to \neg φ) \leftrightarrow (\neg x = B \to \neg φ)$
6		con34b	$⊢ (φ \to x = B) \leftrightarrow (\neg x = B \to \neg φ)$
7	5 6	bitr4i	$⊢ (x \neq B \to \neg φ) \leftrightarrow (φ \to x = B)$
8	7	imbi2i	$⊢ (x \in A \to (x \neq B \to \neg φ)) \leftrightarrow (x \in A \to (φ \to x = B))$
9	2 3 8	3bitri	$⊢ (x \in (A ∖ \{B\}) \to \neg φ) \leftrightarrow (x \in A \to (φ \to x = B))$
10	9	ralbii2	$⊢ \forall x \in (A ∖ \{B\}) \neg φ \leftrightarrow \forall x \in A (φ \to x = B)$

Metamath Proof Explorer