uniex2

Description: The Axiom of Union using the standard abbreviation for union. Given any set x , its union y exists. (Contributed by NM, 4-Jun-2006)

		Ref	Expression
	Assertion	uniex2	$⊢ \exists y y = ⋃ x$

Step	Hyp	Ref	Expression
1		ax-un	$⊢ \exists y \forall z (\exists w (z \in w \land w \in x) \to z \in y)$
2		eluni	$⊢ z \in ⋃ x \leftrightarrow \exists w (z \in w \land w \in x)$
3	2	imbi1i	$⊢ (z \in ⋃ x \to z \in y) \leftrightarrow (\exists w (z \in w \land w \in x) \to z \in y)$
4	3	albii	$⊢ \forall z (z \in ⋃ x \to z \in y) \leftrightarrow \forall z (\exists w (z \in w \land w \in x) \to z \in y)$
5	4	exbii	$⊢ \exists y \forall z (z \in ⋃ x \to z \in y) \leftrightarrow \exists y \forall z (\exists w (z \in w \land w \in x) \to z \in y)$
6	1 5	mpbir	$⊢ \exists y \forall z (z \in ⋃ x \to z \in y)$
7	6	sepexi	$⊢ \exists y \forall z (z \in y \leftrightarrow z \in ⋃ x)$
8		dfcleq	$⊢ y = ⋃ x \leftrightarrow \forall z (z \in y \leftrightarrow z \in ⋃ x)$
9	8	exbii	$⊢ \exists y y = ⋃ x \leftrightarrow \exists y \forall z (z \in y \leftrightarrow z \in ⋃ x)$
10	7 9	mpbir	$⊢ \exists y y = ⋃ x$

Metamath Proof Explorer