Metamath Proof Explorer

Theorem uniex2OLD

Description: Obsolete version of uniex2 as of 14-Jul-2026. (Contributed by NM, 4-Jun-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion uniex2OLD 
|- 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