Metamath Proof Explorer


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 ) )