Metamath Proof Explorer


Theorem intnex

Description: If a class intersection is not a set, it must be the universe. (Contributed by NM, 3-Jul-2005)

Ref Expression
Assertion intnex ( ¬ 𝐴 ∈ V ↔ 𝐴 = V )

Proof

Step Hyp Ref Expression
1 intex ( 𝐴 ≠ ∅ ↔ 𝐴 ∈ V )
2 1 necon1bbii ( ¬ 𝐴 ∈ V ↔ 𝐴 = ∅ )
3 inteq ( 𝐴 = ∅ → 𝐴 = ∅ )
4 int0 ∅ = V
5 3 4 eqtrdi ( 𝐴 = ∅ → 𝐴 = V )
6 2 5 sylbi ( ¬ 𝐴 ∈ V → 𝐴 = V )
7 vprc ¬ V ∈ V
8 eleq1 ( 𝐴 = V → ( 𝐴 ∈ V ↔ V ∈ V ) )
9 7 8 mtbiri ( 𝐴 = V → ¬ 𝐴 ∈ V )
10 6 9 impbii ( ¬ 𝐴 ∈ V ↔ 𝐴 = V )