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\left(x\ne Y\to \phi \right)\leftrightarrow \forall x\in \left(A\setminus \left\{Y\right\}\right)\phi$$

Proof

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