Metamath Proof Explorer


Theorem rniun

Description: The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion rniun
|- ran U_ x e. A B = U_ x e. A ran B

Proof

Step Hyp Ref Expression
1 rexcom4
 |-  ( E. x e. A E. y <. y , z >. e. B <-> E. y E. x e. A <. y , z >. e. B )
2 vex
 |-  z e. _V
3 2 elrn2
 |-  ( z e. ran B <-> E. y <. y , z >. e. B )
4 3 rexbii
 |-  ( E. x e. A z e. ran B <-> E. x e. A E. y <. y , z >. e. B )
5 eliun
 |-  ( <. y , z >. e. U_ x e. A B <-> E. x e. A <. y , z >. e. B )
6 5 exbii
 |-  ( E. y <. y , z >. e. U_ x e. A B <-> E. y E. x e. A <. y , z >. e. B )
7 1 4 6 3bitr4ri
 |-  ( E. y <. y , z >. e. U_ x e. A B <-> E. x e. A z e. ran B )
8 2 elrn2
 |-  ( z e. ran U_ x e. A B <-> E. y <. y , z >. e. U_ x e. A B )
9 eliun
 |-  ( z e. U_ x e. A ran B <-> E. x e. A z e. ran B )
10 7 8 9 3bitr4i
 |-  ( z e. ran U_ x e. A B <-> z e. U_ x e. A ran B )
11 10 eqriv
 |-  ran U_ x e. A B = U_ x e. A ran B