Theorem dfuni2

Description: Alternate definition of class union. (Contributed by NM, 28-Jun-1998)

	Ref	Expression
Assertion	dfuni2	$$⊢\bigcup A=\left\{x|\exists y\in Ax\in y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-uni	$$⊢\bigcup A=\left\{x|\exists y\left(x\in y\wedge y\in A\right)\right\}$$
2		exancom	$$⊢\exists y\left(x\in y\wedge y\in A\right)\leftrightarrow \exists y\left(y\in A\wedge x\in y\right)$$
3		df-rex	$$⊢\exists y\in Ax\in y\leftrightarrow \exists y\left(y\in A\wedge x\in y\right)$$
4	2 3	bitr4i	$$⊢\exists y\left(x\in y\wedge y\in A\right)\leftrightarrow \exists y\in Ax\in y$$
5	4	abbii	$$⊢\left\{x|\exists y\left(x\in y\wedge y\in A\right)\right\}=\left\{x|\exists y\in Ax\in y\right\}$$
6	1 5	eqtri	$$⊢\bigcup A=\left\{x|\exists y\in Ax\in y\right\}$$