Theorem dmiun

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

	Ref	Expression
Assertion	dmiun	$$⊢\mathrm{dom}\bigcup _{x\in A}B=\bigcup _{x\in A}\mathrm{dom}B$$

Proof

Step	Hyp	Ref	Expression
1		rexcom4	$$⊢\exists x\in A\exists z⟨y,z⟩\in B\leftrightarrow \exists z\exists x\in A⟨y,z⟩\in B$$
2		vex	$$⊢y\in \mathrm{V}$$
3	2	eldm2	$$⊢y\in \mathrm{dom}B\leftrightarrow \exists z⟨y,z⟩\in B$$
4	3	rexbii	$$⊢\exists x\in Ay\in \mathrm{dom}B\leftrightarrow \exists x\in A\exists z⟨y,z⟩\in B$$
5		eliun	$$⊢⟨y,z⟩\in \bigcup _{x\in A}B\leftrightarrow \exists x\in A⟨y,z⟩\in B$$
6	5	exbii	$$⊢\exists z⟨y,z⟩\in \bigcup _{x\in A}B\leftrightarrow \exists z\exists x\in A⟨y,z⟩\in B$$
7	1 4 6	3bitr4ri	$$⊢\exists z⟨y,z⟩\in \bigcup _{x\in A}B\leftrightarrow \exists x\in Ay\in \mathrm{dom}B$$
8	2	eldm2	$$⊢y\in \mathrm{dom}\bigcup _{x\in A}B\leftrightarrow \exists z⟨y,z⟩\in \bigcup _{x\in A}B$$
9		eliun	$$⊢y\in \bigcup _{x\in A}\mathrm{dom}B\leftrightarrow \exists x\in Ay\in \mathrm{dom}B$$
10	7 8 9	3bitr4i	$$⊢y\in \mathrm{dom}\bigcup _{x\in A}B\leftrightarrow y\in \bigcup _{x\in A}\mathrm{dom}B$$
11	10	eqriv	$$⊢\mathrm{dom}\bigcup _{x\in A}B=\bigcup _{x\in A}\mathrm{dom}B$$