Theorem 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 \bigcup \left\{x|\phi \right\}\leftrightarrow \exists x\left(A\in x\wedge \phi \right)$$

Proof

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