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

Metamath Proof Explorer

Theorem viin

Description: Indexed intersection with a universal index class. When A doesn't depend on x , this evaluates to A by 19.3 and abid2 . When A = x , this evaluates to (/) by intiin and intv . (Contributed by NM, 11-Sep-2008)

Ref Expression
Assertion viin ⊢ ⋂ x ∈ V A = y | ∀ x y ∈ A

Proof

Step Hyp Ref Expression
1 df-iin ⊢ ⋂ x ∈ V A = y | ∀ x ∈ V y ∈ A
2 ralv ⊢ ∀ x ∈ V y ∈ A ↔ ∀ x y ∈ A
3 2 abbii ⊢ y | ∀ x ∈ V y ∈ A = y | ∀ x y ∈ A
4 1 3 eqtri ⊢ ⋂ x ∈ V A = y | ∀ x y ∈ A