Theorem intex

Description: The intersection of a nonempty class exists. Exercise 5 of TakeutiZaring p. 44 and its converse. (Contributed by NM, 13-Aug-2002)

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

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( A =/= (/) <-> E. x x e. A )
2		intss1	|- ( x e. A -> |^| A C_ x )
3		vex	|- x e. _V
4	3	ssex	|- ( |^| A C_ x -> |^| A e. _V )
5	2 4	syl	|- ( x e. A -> |^| A e. _V )
6	5	exlimiv	|- ( E. x x e. A -> |^| A e. _V )
7	1 6	sylbi	|- ( A =/= (/) -> |^| A e. _V )
8		vprc	|- -. _V e. _V
9		inteq	|- ( A = (/) -> |^| A = |^| (/) )
10		int0	|- |^| (/) = _V
11	9 10	eqtrdi	|- ( A = (/) -> |^| A = _V )
12	11	eleq1d	|- ( A = (/) -> ( |^| A e. _V <-> _V e. _V ) )
13	8 12	mtbiri	|- ( A = (/) -> -. |^| A e. _V )
14	13	necon2ai	|- ( |^| A e. _V -> A =/= (/) )
15	7 14	impbii	|- ( A =/= (/) <-> |^| A e. _V )