This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )