Theorem dmdju

Description: Domain of a disjoint union of non-empty sets. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypothesis	dmdju.1	$$⊢\left(\phi \wedge x\in A\right)\to B\ne \varnothing$$
Assertion	dmdju	$$⊢\phi \to \mathrm{dom}\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		dmdju.1	$$⊢\left(\phi \wedge x\in A\right)\to B\ne \varnothing$$
2		dmiun	$$⊢\mathrm{dom}\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)=\bigcup _{x\in A}\mathrm{dom}\left(\left\{x\right\}\times B\right)$$
3		dmxp	$$⊢B\ne \varnothing \to \mathrm{dom}\left(\left\{x\right\}\times B\right)=\left\{x\right\}$$
4	1 3	syl	$$⊢\left(\phi \wedge x\in A\right)\to \mathrm{dom}\left(\left\{x\right\}\times B\right)=\left\{x\right\}$$
5	4	iuneq2dv	$$⊢\phi \to \bigcup _{x\in A}\mathrm{dom}\left(\left\{x\right\}\times B\right)=\bigcup _{x\in A}\left\{x\right\}$$
6	2 5	eqtrid	$$⊢\phi \to \mathrm{dom}\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)=\bigcup _{x\in A}\left\{x\right\}$$
7		iunid	$$⊢\bigcup _{x\in A}\left\{x\right\}=A$$
8	6 7	eqtrdi	$$⊢\phi \to \mathrm{dom}\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)=A$$