dmdju

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

		Ref	Expression
	Hypothesis	dmdju.1	$⊢ (φ \land x \in A) \to B \neq \emptyset$
	Assertion	dmdju	$⊢ φ \to dom ⋃_{x \in A} (\{x\} \times B) = A$

Step	Hyp	Ref	Expression
1		dmdju.1	$⊢ (φ \land x \in A) \to B \neq \emptyset$
2		dmiun	$⊢ dom ⋃_{x \in A} (\{x\} \times B) = ⋃_{x \in A} dom (\{x\} \times B)$
3		dmxp	$⊢ B \neq \emptyset \to dom (\{x\} \times B) = \{x\}$
4	1 3	syl	$⊢ (φ \land x \in A) \to dom (\{x\} \times B) = \{x\}$
5	4	iuneq2dv	$⊢ φ \to ⋃_{x \in A} dom (\{x\} \times B) = ⋃_{x \in A} \{x\}$
6	2 5	eqtrid	$⊢ φ \to dom ⋃_{x \in A} (\{x\} \times B) = ⋃_{x \in A} \{x\}$
7		iunid	$⊢ ⋃_{x \in A} \{x\} = A$
8	6 7	eqtrdi	$⊢ φ \to dom ⋃_{x \in A} (\{x\} \times B) = A$

Metamath Proof Explorer