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

Metamath Proof Explorer

Theorem iotan0

Description: Representation of "the unique element such that ph " with a class expression A which is not the empty set (that means that "the unique element such that ph " exists). (Contributed by AV, 30-Jan-2024)

Ref Expression
Hypothesis iotan0.1 
|- ( x = A -> ( ph <-> ps ) )
Assertion iotan0 
|- ( ( A e. V /\ A =/= (/) /\ A = ( iota x ph ) ) -> ps )

Proof

Step Hyp Ref Expression
1 iotan0.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 pm13.18 
 |-  ( ( A = ( iota x ph ) /\ A =/= (/) ) -> ( iota x ph ) =/= (/) )
3 2 expcom 
 |-  ( A =/= (/) -> ( A = ( iota x ph ) -> ( iota x ph ) =/= (/) ) )
4 iotanul 
 |-  ( -. E! x ph -> ( iota x ph ) = (/) )
5 4 necon1ai 
 |-  ( ( iota x ph ) =/= (/) -> E! x ph )
6 3 5 syl6 
 |-  ( A =/= (/) -> ( A = ( iota x ph ) -> E! x ph ) )
7 6 a1i 
 |-  ( A e. V -> ( A =/= (/) -> ( A = ( iota x ph ) -> E! x ph ) ) )
8 7 3imp 
 |-  ( ( A e. V /\ A =/= (/) /\ A = ( iota x ph ) ) -> E! x ph )
9 eqcom 
 |-  ( A = ( iota x ph ) <-> ( iota x ph ) = A )
10 1 iota2 
 |-  ( ( A e. V /\ E! x ph ) -> ( ps <-> ( iota x ph ) = A ) )
11 10 biimprd 
 |-  ( ( A e. V /\ E! x ph ) -> ( ( iota x ph ) = A -> ps ) )
12 9 11 biimtrid 
 |-  ( ( A e. V /\ E! x ph ) -> ( A = ( iota x ph ) -> ps ) )
13 12 impancom 
 |-  ( ( A e. V /\ A = ( iota x ph ) ) -> ( E! x ph -> ps ) )
14 13 3adant2 
 |-  ( ( A e. V /\ A =/= (/) /\ A = ( iota x ph ) ) -> ( E! x ph -> ps ) )
15 8 14 mpd 
 |-  ( ( A e. V /\ A =/= (/) /\ A = ( iota x ph ) ) -> ps )