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