eluniab

Description: Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994) (Revised by Mario Carneiro, 14-Nov-2016)

		Ref	Expression
	Assertion	eluniab	$⊢ A \in ⋃ \{x \| φ\} \leftrightarrow \exists x (A \in x \land φ)$

Step	Hyp	Ref	Expression
1		eluni	$⊢ A \in ⋃ \{x \| φ\} \leftrightarrow \exists y (A \in y \land y \in \{x \| φ\})$
2		nfv	$⊢ Ⅎ x A \in y$
3		nfsab1	$⊢ Ⅎ x y \in \{x \| φ\}$
4	2 3	nfan	$⊢ Ⅎ x (A \in y \land y \in \{x \| φ\})$
5		nfv	$⊢ Ⅎ y (A \in x \land φ)$
6		eleq2w	$⊢ y = x \to (A \in y \leftrightarrow A \in x)$
7		eleq1w	$⊢ y = x \to (y \in \{x \| φ\} \leftrightarrow x \in \{x \| φ\})$
8		abid	$⊢ x \in \{x \| φ\} \leftrightarrow φ$
9	7 8	bitrdi	$⊢ y = x \to (y \in \{x \| φ\} \leftrightarrow φ)$
10	6 9	anbi12d	$⊢ y = x \to ((A \in y \land y \in \{x \| φ\}) \leftrightarrow (A \in x \land φ))$
11	4 5 10	cbvexv1	$⊢ \exists y (A \in y \land y \in \{x \| φ\}) \leftrightarrow \exists x (A \in x \land φ)$
12	1 11	bitri	$⊢ A \in ⋃ \{x \| φ\} \leftrightarrow \exists x (A \in x \land φ)$

Metamath Proof Explorer