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

Metamath Proof Explorer

Theorem dfiin3

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

Ref Expression
Hypothesis dfiun3.1 ⊢ 𝐵 ∈ V
Assertion dfiin3 ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )

Proof

Step Hyp Ref Expression
1 dfiun3.1 ⊢ 𝐵 ∈ V
2 dfiin3g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
3 1 a1i ⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ V )
4 2 3 mprg ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )