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 ( 𝐴 ≠ ∅ ↔ 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 n0 ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥𝐴 )
2 intss1 ( 𝑥𝐴 𝐴𝑥 )
3 vex 𝑥 ∈ V
4 3 ssex ( 𝐴𝑥 𝐴 ∈ V )
5 2 4 syl ( 𝑥𝐴 𝐴 ∈ V )
6 5 exlimiv ( ∃ 𝑥 𝑥𝐴 𝐴 ∈ V )
7 1 6 sylbi ( 𝐴 ≠ ∅ → 𝐴 ∈ V )
8 vprc ¬ V ∈ V
9 inteq ( 𝐴 = ∅ → 𝐴 = ∅ )
10 int0 ∅ = V
11 9 10 eqtrdi ( 𝐴 = ∅ → 𝐴 = V )
12 11 eleq1d ( 𝐴 = ∅ → ( 𝐴 ∈ V ↔ V ∈ V ) )
13 8 12 mtbiri ( 𝐴 = ∅ → ¬ 𝐴 ∈ V )
14 13 necon2ai ( 𝐴 ∈ V → 𝐴 ≠ ∅ )
15 7 14 impbii ( 𝐴 ≠ ∅ ↔ 𝐴 ∈ V )