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 ( 𝑥𝐴𝐵 )