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 V

Proof

Step Hyp Ref Expression
1 n0 A x x A
2 intss1 x A A x
3 vex x V
4 3 ssex A x A V
5 2 4 syl x A A V
6 5 exlimiv x x A A V
7 1 6 sylbi A A V
8 vprc ¬ V V
9 inteq A = A =
10 int0 = V
11 9 10 syl6eq A = A = V
12 11 eleq1d A = A V V V
13 8 12 mtbiri A = ¬ A V
14 13 necon2ai A V A
15 7 14 impbii A A V