Metamath Proof Explorer


Theorem dfiun3g

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

Ref Expression
Assertion dfiun3g ( ∀ 𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = ran ( 𝑥𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 dfiun2g ( ∀ 𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } )
2 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
3 2 rnmpt ran ( 𝑥𝐴𝐵 ) = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 }
4 3 unieqi ran ( 𝑥𝐴𝐵 ) = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 }
5 1 4 eqtr4di ( ∀ 𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = ran ( 𝑥𝐴𝐵 ) )