Metamath Proof Explorer

Theorem dmuni

Description: The domain of a union. Part of Exercise 8 of Enderton p. 41. (Contributed by NM, 3-Feb-2004)

		Ref	Expression
	Assertion	dmuni	$⊢ dom ⋃ A = ⋃_{x \in A} dom x$

Proof

Step	Hyp	Ref	Expression
1		excom	$⊢ \exists z \exists x (⟨y, z⟩ \in x \land x \in A) \leftrightarrow \exists x \exists z (⟨y, z⟩ \in x \land x \in A)$
2		ancom	$⊢ (\exists z ⟨y, z⟩ \in x \land x \in A) \leftrightarrow (x \in A \land \exists z ⟨y, z⟩ \in x)$
3		19.41v	$⊢ \exists z (⟨y, z⟩ \in x \land x \in A) \leftrightarrow (\exists z ⟨y, z⟩ \in x \land x \in A)$
4		vex	$⊢ y \in V$
5	4	eldm2	$⊢ y \in dom x \leftrightarrow \exists z ⟨y, z⟩ \in x$
6	5	anbi2i	$⊢ (x \in A \land y \in dom x) \leftrightarrow (x \in A \land \exists z ⟨y, z⟩ \in x)$
7	2 3 6	3bitr4i	$⊢ \exists z (⟨y, z⟩ \in x \land x \in A) \leftrightarrow (x \in A \land y \in dom x)$
8	7	exbii	$⊢ \exists x \exists z (⟨y, z⟩ \in x \land x \in A) \leftrightarrow \exists x (x \in A \land y \in dom x)$
9	1 8	bitri	$⊢ \exists z \exists x (⟨y, z⟩ \in x \land x \in A) \leftrightarrow \exists x (x \in A \land y \in dom x)$
10		eluni	$⊢ ⟨y, z⟩ \in ⋃ A \leftrightarrow \exists x (⟨y, z⟩ \in x \land x \in A)$
11	10	exbii	$⊢ \exists z ⟨y, z⟩ \in ⋃ A \leftrightarrow \exists z \exists x (⟨y, z⟩ \in x \land x \in A)$
12		df-rex	$⊢ \exists x \in A y \in dom x \leftrightarrow \exists x (x \in A \land y \in dom x)$
13	9 11 12	3bitr4i	$⊢ \exists z ⟨y, z⟩ \in ⋃ A \leftrightarrow \exists x \in A y \in dom x$
14	4	eldm2	$⊢ y \in dom ⋃ A \leftrightarrow \exists z ⟨y, z⟩ \in ⋃ A$
15		eliun	$⊢ y \in ⋃_{x \in A} dom x \leftrightarrow \exists x \in A y \in dom x$
16	13 14 15	3bitr4i	$⊢ y \in dom ⋃ A \leftrightarrow y \in ⋃_{x \in A} dom x$
17	16	eqriv	$⊢ dom ⋃ A = ⋃_{x \in A} dom x$