Theorem elnev

Description: Any set that contains one element less than the universe is not equal to it. (Contributed by Andrew Salmon, 16-Jun-2011)

	Ref	Expression
Assertion	elnev	$$⊢A\in \mathrm{V}\leftrightarrow \left\{x|\neg x=A\right\}\ne \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		isset	$$⊢A\in \mathrm{V}\leftrightarrow \exists xx=A$$
2		df-v	$$⊢\mathrm{V}=\left\{x|x=x\right\}$$
3	2	eqeq2i	$$⊢\left\{x|\neg x=A\right\}=\mathrm{V}\leftrightarrow \left\{x|\neg x=A\right\}=\left\{x|x=x\right\}$$
4		abbib	$$⊢\left\{x|\neg x=A\right\}=\left\{x|x=x\right\}\leftrightarrow \forall x\left(\neg x=A\leftrightarrow x=x\right)$$
5		equid	$$⊢x=x$$
6	5	tbt	$$⊢\neg x=A\leftrightarrow \left(\neg x=A\leftrightarrow x=x\right)$$
7	6	albii	$$⊢\forall x\neg x=A\leftrightarrow \forall x\left(\neg x=A\leftrightarrow x=x\right)$$
8		alnex	$$⊢\forall x\neg x=A\leftrightarrow \neg \exists xx=A$$
9	4 7 8	3bitr2i	$$⊢\left\{x|\neg x=A\right\}=\left\{x|x=x\right\}\leftrightarrow \neg \exists xx=A$$
10	3 9	bitri	$$⊢\left\{x|\neg x=A\right\}=\mathrm{V}\leftrightarrow \neg \exists xx=A$$
11	10	necon2abii	$$⊢\exists xx=A\leftrightarrow \left\{x|\neg x=A\right\}\ne \mathrm{V}$$
12	1 11	bitri	$$⊢A\in \mathrm{V}\leftrightarrow \left\{x|\neg x=A\right\}\ne \mathrm{V}$$