Theorem 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	|- E. y y = U. x

Proof

Step	Hyp	Ref	Expression
1		ax-un	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
2		eluni	|- ( z e. U. x <-> E. w ( z e. w /\ w e. x ) )
3	2	imbi1i	|- ( ( z e. U. x -> z e. y ) <-> ( E. w ( z e. w /\ w e. x ) -> z e. y ) )
4	3	albii	|- ( A. z ( z e. U. x -> z e. y ) <-> A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) )
5	4	exbii	|- ( E. y A. z ( z e. U. x -> z e. y ) <-> E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) )
6	1 5	mpbir	|- E. y A. z ( z e. U. x -> z e. y )
7	6	bm1.3ii	|- E. y A. z ( z e. y <-> z e. U. x )
8		dfcleq	|- ( y = U. x <-> A. z ( z e. y <-> z e. U. x ) )
9	8	exbii	|- ( E. y y = U. x <-> E. y A. z ( z e. y <-> z e. U. x ) )
10	7 9	mpbir	|- E. y y = U. x