Theorem dmiun

Description: The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Assertion	dmiun	|- dom U_ x e. A B = U_ x e. A dom B

Proof

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