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

Metamath Proof Explorer

Theorem raldifsnb

Description: Restricted universal quantification on a class difference with a singleton in terms of an implication. (Contributed by Alexander van der Vekens, 26-Jan-2018)

		Ref	Expression
	Assertion	raldifsnb	$⊢ \forall x \in A (x \neq Y \to φ) \leftrightarrow \forall x \in (A ∖ \{Y\}) φ$

Proof

Step	Hyp	Ref	Expression
1		velsn	$⊢ x \in \{Y\} \leftrightarrow x = Y$
2		nnel	$⊢ \neg x \notin \{Y\} \leftrightarrow x \in \{Y\}$
3		nne	$⊢ \neg x \neq Y \leftrightarrow x = Y$
4	1 2 3	3bitr4ri	$⊢ \neg x \neq Y \leftrightarrow \neg x \notin \{Y\}$
5	4	con4bii	$⊢ x \neq Y \leftrightarrow x \notin \{Y\}$
6	5	imbi1i	$⊢ (x \neq Y \to φ) \leftrightarrow (x \notin \{Y\} \to φ)$
7	6	ralbii	$⊢ \forall x \in A (x \neq Y \to φ) \leftrightarrow \forall x \in A (x \notin \{Y\} \to φ)$
8		raldifb	$⊢ \forall x \in A (x \notin \{Y\} \to φ) \leftrightarrow \forall x \in (A ∖ \{Y\}) φ$
9	7 8	bitri	$⊢ \forall x \in A (x \neq Y \to φ) \leftrightarrow \forall x \in (A ∖ \{Y\}) φ$