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

Metamath Proof Explorer

Theorem dfiin3g

Description: Alternate definition of indexed intersection when B is a set. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion dfiin3g ⊢ ∀ x ∈ A B ∈ C → ⋂ x ∈ A B = ⋂ ran ⁡ x ∈ A ⟼ B

Proof

Step Hyp Ref Expression
1 dfiin2g ⊢ ∀ x ∈ A B ∈ C → ⋂ x ∈ A B = ⋂ y | ∃ x ∈ A y = B
2 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
3 2 rnmpt ⊢ ran ⁡ x ∈ A ⟼ B = y | ∃ x ∈ A y = B
4 3 inteqi ⊢ ⋂ ran ⁡ x ∈ A ⟼ B = ⋂ y | ∃ x ∈ A y = B
5 1 4 eqtr4di ⊢ ∀ x ∈ A B ∈ C → ⋂ x ∈ A B = ⋂ ran ⁡ x ∈ A ⟼ B