Theorem intnex

Description: If a class intersection is not a set, it must be the universe. (Contributed by NM, 3-Jul-2005)

	Ref	Expression
Assertion	intnex	|- ( -. |^| A e. _V <-> |^| A = _V )

Proof

Step	Hyp	Ref	Expression
1		intex	|- ( A =/= (/) <-> |^| A e. _V )
2	1	necon1bbii	|- ( -. |^| A e. _V <-> A = (/) )
3		inteq	|- ( A = (/) -> |^| A = |^| (/) )
4		int0	|- |^| (/) = _V
5	3 4	eqtrdi	|- ( A = (/) -> |^| A = _V )
6	2 5	sylbi	|- ( -. |^| A e. _V -> |^| A = _V )
7		vprc	|- -. _V e. _V
8		eleq1	|- ( |^| A = _V -> ( |^| A e. _V <-> _V e. _V ) )
9	7 8	mtbiri	|- ( |^| A = _V -> -. |^| A e. _V )
10	6 9	impbii	|- ( -. |^| A e. _V <-> |^| A = _V )