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 )