Metamath Proof Explorer

Theorem int0

Description: The intersection of the empty set is the universal class. Exercise 2 of TakeutiZaring p. 44. (Contributed by NM, 18-Aug-1993) (Proof shortened by JJ, 26-Jul-2021)

Ref Expression
Assertion int0 ⊢ ⋂ ∅ = V

Proof

Step Hyp Ref Expression
1 ral0 ⊢ ∀ x ∈ ∅ y ∈ x
2 vex ⊢ y ∈ V
3 2 elint2 ⊢ y ∈ ⋂ ∅ ↔ ∀ x ∈ ∅ y ∈ x
4 1 3 mpbir ⊢ y ∈ ⋂ ∅
5 4 2 2th ⊢ y ∈ ⋂ ∅ ↔ y ∈ V
6 5 eqriv ⊢ ⋂ ∅ = V