This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 sepexi 
 |-  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