Theorem iota5f

Description: A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017)

	Ref	Expression
Hypotheses	iota5f.1	|- F/ x ph
	iota5f.2	|- F/_ x A
	iota5f.3	|- ( ( ph /\ A e. V ) -> ( ps <-> x = A ) )
Assertion	iota5f	|- ( ( ph /\ A e. V ) -> ( iota x ps ) = A )

Proof

Step	Hyp	Ref	Expression
1		iota5f.1	|- F/ x ph
2		iota5f.2	|- F/_ x A
3		iota5f.3	|- ( ( ph /\ A e. V ) -> ( ps <-> x = A ) )
4	2	nfel1	|- F/ x A e. V
5	1 4	nfan	|- F/ x ( ph /\ A e. V )
6	5 3	alrimi	|- ( ( ph /\ A e. V ) -> A. x ( ps <-> x = A ) )
7	2	nfeq2	|- F/ x y = A
8		eqeq2	|- ( y = A -> ( x = y <-> x = A ) )
9	8	bibi2d	|- ( y = A -> ( ( ps <-> x = y ) <-> ( ps <-> x = A ) ) )
10	7 9	albid	|- ( y = A -> ( A. x ( ps <-> x = y ) <-> A. x ( ps <-> x = A ) ) )
11		eqeq2	|- ( y = A -> ( ( iota x ps ) = y <-> ( iota x ps ) = A ) )
12	10 11	imbi12d	|- ( y = A -> ( ( A. x ( ps <-> x = y ) -> ( iota x ps ) = y ) <-> ( A. x ( ps <-> x = A ) -> ( iota x ps ) = A ) ) )
13		iotaval	|- ( A. x ( ps <-> x = y ) -> ( iota x ps ) = y )
14	12 13	vtoclg	|- ( A e. V -> ( A. x ( ps <-> x = A ) -> ( iota x ps ) = A ) )
15	14	adantl	|- ( ( ph /\ A e. V ) -> ( A. x ( ps <-> x = A ) -> ( iota x ps ) = A ) )
16	6 15	mpd	|- ( ( ph /\ A e. V ) -> ( iota x ps ) = A )