Theorem iota2

Description: The unique element such that ph . (Contributed by Jeff Madsen, 1-Jun-2011) (Revised by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypothesis	iota2.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	iota2	|- ( ( A e. B /\ E! x ph ) -> ( ps <-> ( iota x ph ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		iota2.1	|- ( x = A -> ( ph <-> ps ) )
2		elex	|- ( A e. B -> A e. _V )
3		simpl	|- ( ( A e. _V /\ E! x ph ) -> A e. _V )
4		simpr	|- ( ( A e. _V /\ E! x ph ) -> E! x ph )
5	1	adantl	|- ( ( ( A e. _V /\ E! x ph ) /\ x = A ) -> ( ph <-> ps ) )
6		nfv	|- F/ x A e. _V
7		nfeu1	|- F/ x E! x ph
8	6 7	nfan	|- F/ x ( A e. _V /\ E! x ph )
9		nfvd	|- ( ( A e. _V /\ E! x ph ) -> F/ x ps )
10		nfcvd	|- ( ( A e. _V /\ E! x ph ) -> F/_ x A )
11	3 4 5 8 9 10	iota2df	|- ( ( A e. _V /\ E! x ph ) -> ( ps <-> ( iota x ph ) = A ) )
12	2 11	sylan	|- ( ( A e. B /\ E! x ph ) -> ( ps <-> ( iota x ph ) = A ) )