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 e. _V <-> { x | -. x = A } =/= _V )

Proof

Step	Hyp	Ref	Expression
1		isset	|- ( A e. _V <-> E. x x = A )
2		df-v	|- _V = { x | x = x }
3	2	eqeq2i	|- ( { x | -. x = A } = _V <-> { x | -. x = A } = { x | x = x } )
4		abbib	|- ( { x | -. x = A } = { x | x = x } <-> A. x ( -. x = A <-> x = x ) )
5		equid	|- x = x
6	5	tbt	|- ( -. x = A <-> ( -. x = A <-> x = x ) )
7	6	albii	|- ( A. x -. x = A <-> A. x ( -. x = A <-> x = x ) )
8		alnex	|- ( A. x -. x = A <-> -. E. x x = A )
9	4 7 8	3bitr2i	|- ( { x | -. x = A } = { x | x = x } <-> -. E. x x = A )
10	3 9	bitri	|- ( { x | -. x = A } = _V <-> -. E. x x = A )
11	10	necon2abii	|- ( E. x x = A <-> { x | -. x = A } =/= _V )
12	1 11	bitri	|- ( A e. _V <-> { x | -. x = A } =/= _V )