iunab

Description: The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004)

		Ref	Expression
	Assertion	iunab	$⊢ ⋃_{x \in A} \{y \| φ\} = \{y \| \exists x \in A φ\}$

Step	Hyp	Ref	Expression
1		nfcv	$⊢ \underline{Ⅎ} y A$
2		nfab1	$⊢ \underline{Ⅎ} y \{y \| φ\}$
3	1 2	nfiun	$⊢ \underline{Ⅎ} y ⋃_{x \in A} \{y \| φ\}$
4		nfab1	$⊢ \underline{Ⅎ} y \{y \| \exists x \in A φ\}$
5	3 4	cleqf	$⊢ ⋃_{x \in A} \{y \| φ\} = \{y \| \exists x \in A φ\} \leftrightarrow \forall y (y \in ⋃_{x \in A} \{y \| φ\} \leftrightarrow y \in \{y \| \exists x \in A φ\})$
6		abid	$⊢ y \in \{y \| φ\} \leftrightarrow φ$
7	6	rexbii	$⊢ \exists x \in A y \in \{y \| φ\} \leftrightarrow \exists x \in A φ$
8		eliun	$⊢ y \in ⋃_{x \in A} \{y \| φ\} \leftrightarrow \exists x \in A y \in \{y \| φ\}$
9		abid	$⊢ y \in \{y \| \exists x \in A φ\} \leftrightarrow \exists x \in A φ$
10	7 8 9	3bitr4i	$⊢ y \in ⋃_{x \in A} \{y \| φ\} \leftrightarrow y \in \{y \| \exists x \in A φ\}$
11	5 10	mpgbir	$⊢ ⋃_{x \in A} \{y \| φ\} = \{y \| \exists x \in A φ\}$

Metamath Proof Explorer