Theorem vnex

Description: The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005)

	Ref	Expression
Assertion	vnex	|- -. E. x x = _V

Proof

Step	Hyp	Ref	Expression
1		nalset	|- -. E. x A. y y e. x
2		vex	|- y e. _V
3	2	tbt	|- ( y e. x <-> ( y e. x <-> y e. _V ) )
4	3	albii	|- ( A. y y e. x <-> A. y ( y e. x <-> y e. _V ) )
5		dfcleq	|- ( x = _V <-> A. y ( y e. x <-> y e. _V ) )
6	4 5	bitr4i	|- ( A. y y e. x <-> x = _V )
7	6	exbii	|- ( E. x A. y y e. x <-> E. x x = _V )
8	1 7	mtbi	|- -. E. x x = _V