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

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