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

Metamath Proof Explorer

Theorem iota5

Description: A method for computing iota. (Contributed by NM, 17-Sep-2013)

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

Proof

Step Hyp Ref Expression
1 iota5.1 
 |-  ( ( ph /\ A e. V ) -> ( ps <-> x = A ) )
2 1 alrimiv 
 |-  ( ( ph /\ A e. V ) -> A. x ( ps <-> x = A ) )
3 eqeq2 
 |-  ( y = A -> ( x = y <-> x = A ) )
4 3 bibi2d 
 |-  ( y = A -> ( ( ps <-> x = y ) <-> ( ps <-> x = A ) ) )
5 4 albidv 
 |-  ( y = A -> ( A. x ( ps <-> x = y ) <-> A. x ( ps <-> x = A ) ) )
6 eqeq2 
 |-  ( y = A -> ( ( iota x ps ) = y <-> ( iota x ps ) = A ) )
7 5 6 imbi12d 
 |-  ( y = A -> ( ( A. x ( ps <-> x = y ) -> ( iota x ps ) = y ) <-> ( A. x ( ps <-> x = A ) -> ( iota x ps ) = A ) ) )
8 iotaval 
 |-  ( A. x ( ps <-> x = y ) -> ( iota x ps ) = y )
9 7 8 vtoclg 
 |-  ( A e. V -> ( A. x ( ps <-> x = A ) -> ( iota x ps ) = A ) )
10 9 adantl 
 |-  ( ( ph /\ A e. V ) -> ( A. x ( ps <-> x = A ) -> ( iota x ps ) = A ) )
11 2 10 mpd 
 |-  ( ( ph /\ A e. V ) -> ( iota x ps ) = A )