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) (Proof shortened by BJ, 14-Jul-2026)

	Ref	Expression
Assertion	uniex2	|- E. y y = U. x

Proof

Step	Hyp	Ref	Expression
1		axun2	|- E. y A. z ( z e. y <-> E. w ( z e. w /\ w e. x ) )
2		eluni	|- ( z e. U. x <-> E. w ( z e. w /\ w e. x ) )
3	2	bibi2i	|- ( ( z e. y <-> z e. U. x ) <-> ( z e. y <-> E. w ( z e. w /\ w e. x ) ) )
4	3	albii	|- ( A. z ( z e. y <-> z e. U. x ) <-> A. z ( z e. y <-> E. w ( z e. w /\ w e. x ) ) )
5	4	exbii	|- ( E. y A. z ( z e. y <-> z e. U. x ) <-> E. y A. z ( z e. y <-> E. w ( z e. w /\ w e. x ) ) )
6	1 5	mpbir	|- E. y A. z ( z e. y <-> z e. U. x )
7		dfcleq	|- ( y = U. x <-> A. z ( z e. y <-> z e. U. x ) )
8	7	biimpri	|- ( A. z ( z e. y <-> z e. U. x ) -> y = U. x )
9	6 8	eximii	|- E. y y = U. x