bnj1400

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	bnj1400.1	$⊢ y \in A \to \forall x y \in A$
	Assertion	bnj1400	$⊢ dom ⋃ A = ⋃_{x \in A} dom x$

Step	Hyp	Ref	Expression
1		bnj1400.1	$⊢ y \in A \to \forall x y \in A$
2		dmuni	$⊢ dom ⋃ A = ⋃_{z \in A} dom z$
3		df-iun	$⊢ ⋃_{x \in A} dom x = \{y \| \exists x \in A y \in dom x\}$
4		df-iun	$⊢ ⋃_{z \in A} dom z = \{y \| \exists z \in A y \in dom z\}$
5	1	nfcii	$⊢ \underline{Ⅎ} x A$
6		nfcv	$⊢ \underline{Ⅎ} z A$
7		nfv	$⊢ Ⅎ z y \in dom x$
8		nfv	$⊢ Ⅎ x y \in dom z$
9		dmeq	$⊢ x = z \to dom x = dom z$
10	9	eleq2d	$⊢ x = z \to (y \in dom x \leftrightarrow y \in dom z)$
11	5 6 7 8 10	cbvrexfw	$⊢ \exists x \in A y \in dom x \leftrightarrow \exists z \in A y \in dom z$
12	11	abbii	$⊢ \{y \| \exists x \in A y \in dom x\} = \{y \| \exists z \in A y \in dom z\}$
13	4 12	eqtr4i	$⊢ ⋃_{z \in A} dom z = \{y \| \exists x \in A y \in dom x\}$
14	3 13	eqtr4i	$⊢ ⋃_{x \in A} dom x = ⋃_{z \in A} dom z$
15	2 14	eqtr4i	$⊢ dom ⋃ A = ⋃_{x \in A} dom x$

Metamath Proof Explorer