Theorem axun2

Description: A variant of the Axiom of Union ax-un . For any set x , there exists a set y whose members are exactly the members of the members of x i.e. the union of x . Axiom Union of BellMachover p. 466. (Contributed by NM, 4-Jun-2006)

	Ref	Expression
Assertion	axun2	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \exists w\left(z\in w\wedge w\in x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-un	$$⊢\exists y\forall z\left(\exists w\left(z\in w\wedge w\in x\right)\to z\in y\right)$$
2	1	bm1.3ii	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \exists w\left(z\in w\wedge w\in x\right)\right)$$