Theorem dmdju

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

	Ref	Expression
Hypothesis	dmdju.1	|- ( ( ph /\ x e. A ) -> B =/= (/) )
Assertion	dmdju	|- ( ph -> dom U_ x e. A ( { x } X. B ) = A )

Proof

Step	Hyp	Ref	Expression
1		dmdju.1	|- ( ( ph /\ x e. A ) -> B =/= (/) )
2		dmiun	|- dom U_ x e. A ( { x } X. B ) = U_ x e. A dom ( { x } X. B )
3		dmxp	|- ( B =/= (/) -> dom ( { x } X. B ) = { x } )
4	1 3	syl	|- ( ( ph /\ x e. A ) -> dom ( { x } X. B ) = { x } )
5	4	iuneq2dv	|- ( ph -> U_ x e. A dom ( { x } X. B ) = U_ x e. A { x } )
6	2 5	eqtrid	|- ( ph -> dom U_ x e. A ( { x } X. B ) = U_ x e. A { x } )
7		iunid	|- U_ x e. A { x } = A
8	6 7	eqtrdi	|- ( ph -> dom U_ x e. A ( { x } X. B ) = A )