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

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