Metamath Proof Explorer

Theorem dfiun3

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

Ref Expression
Hypothesis dfiun3.1 
|- B e. _V
Assertion dfiun3 
|- U_ x e. A B = U. ran ( x e. A |-> B )

Proof

Step Hyp Ref Expression
1 dfiun3.1 
 |-  B e. _V
2 dfiun3g 
 |-  ( A. x e. A B e. _V -> U_ x e. A B = U. ran ( x e. A |-> B ) )
3 1 a1i 
 |-  ( x e. A -> B e. _V )
4 2 3 mprg 
 |-  U_ x e. A B = U. ran ( x e. A |-> B )