Metamath Proof Explorer

Theorem iotaexeu

Description: The iota class exists. This theorem does not require ax-nul for its proof. (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotaexeu 
|- ( E! x ph -> ( iota x ph ) e. _V )

Proof

Step Hyp Ref Expression
1 iotaval 
 |-  ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )
2 1 eqcomd 
 |-  ( A. x ( ph <-> x = y ) -> y = ( iota x ph ) )
3 2 eximi 
 |-  ( E. y A. x ( ph <-> x = y ) -> E. y y = ( iota x ph ) )
4 eu6 
 |-  ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
5 isset 
 |-  ( ( iota x ph ) e. _V <-> E. y y = ( iota x ph ) )
6 3 4 5 3imtr4i 
 |-  ( E! x ph -> ( iota x ph ) e. _V )