# 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}\ne \varnothing ↔\bigcap {A}\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 n0 ${⊢}{A}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
2 intss1 ${⊢}{x}\in {A}\to \bigcap {A}\subseteq {x}$
3 vex ${⊢}{x}\in \mathrm{V}$
4 3 ssex ${⊢}\bigcap {A}\subseteq {x}\to \bigcap {A}\in \mathrm{V}$
5 2 4 syl ${⊢}{x}\in {A}\to \bigcap {A}\in \mathrm{V}$
6 5 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}\to \bigcap {A}\in \mathrm{V}$
7 1 6 sylbi ${⊢}{A}\ne \varnothing \to \bigcap {A}\in \mathrm{V}$
8 vprc ${⊢}¬\mathrm{V}\in \mathrm{V}$
9 inteq ${⊢}{A}=\varnothing \to \bigcap {A}=\bigcap \varnothing$
10 int0 ${⊢}\bigcap \varnothing =\mathrm{V}$
11 9 10 syl6eq ${⊢}{A}=\varnothing \to \bigcap {A}=\mathrm{V}$
12 11 eleq1d ${⊢}{A}=\varnothing \to \left(\bigcap {A}\in \mathrm{V}↔\mathrm{V}\in \mathrm{V}\right)$
13 8 12 mtbiri ${⊢}{A}=\varnothing \to ¬\bigcap {A}\in \mathrm{V}$
14 13 necon2ai ${⊢}\bigcap {A}\in \mathrm{V}\to {A}\ne \varnothing$
15 7 14 impbii ${⊢}{A}\ne \varnothing ↔\bigcap {A}\in \mathrm{V}$