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

Metamath Proof Explorer

Theorem iinconst

Description: Indexed intersection of a constant class, i.e. where B does not depend on x . (Contributed by Mario Carneiro, 6-Feb-2015)

Ref Expression
Assertion iinconst ⊢ A ≠ ∅ → ⋂ x ∈ A B = B

Proof

Step Hyp Ref Expression
1 eliin ⊢ y ∈ V → y ∈ ⋂ x ∈ A B ↔ ∀ x ∈ A y ∈ B
2 1 elv ⊢ y ∈ ⋂ x ∈ A B ↔ ∀ x ∈ A y ∈ B
3 r19.3rzv ⊢ A ≠ ∅ → y ∈ B ↔ ∀ x ∈ A y ∈ B
4 2 3 bitr4id ⊢ A ≠ ∅ → y ∈ ⋂ x ∈ A B ↔ y ∈ B
5 4 eqrdv ⊢ A ≠ ∅ → ⋂ x ∈ A B = B