This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0iin

Description: An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005)

Ref Expression
Assertion 0iin ⊢ ⋂ x ∈ ∅ A = V

Proof

Step Hyp Ref Expression
1 df-iin ⊢ ⋂ x ∈ ∅ A = y | ∀ x ∈ ∅ y ∈ A
2 vex ⊢ y ∈ V
3 ral0 ⊢ ∀ x ∈ ∅ y ∈ A
4 2 3 2th ⊢ y ∈ V ↔ ∀ x ∈ ∅ y ∈ A
5 4 eqabi ⊢ V = y | ∀ x ∈ ∅ y ∈ A
6 1 5 eqtr4i ⊢ ⋂ x ∈ ∅ A = V