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

Proof

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