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

Metamath Proof Explorer

Theorem iota2df

Description: A condition that allows to represent "the unique element such that ph " with a class expression A . (Contributed by NM, 30-Dec-2014)

Ref Expression
Hypotheses iota2df.1 
|- ( ph -> B e. V )
iota2df.2 
|- ( ph -> E! x ps )
iota2df.3 
|- ( ( ph /\ x = B ) -> ( ps <-> ch ) )
iota2df.4 
|- F/ x ph
iota2df.5 
|- ( ph -> F/ x ch )
iota2df.6 
|- ( ph -> F/_ x B )
Assertion iota2df 
|- ( ph -> ( ch <-> ( iota x ps ) = B ) )

Proof

Step Hyp Ref Expression
1 iota2df.1 
 |-  ( ph -> B e. V )
2 iota2df.2 
 |-  ( ph -> E! x ps )
3 iota2df.3 
 |-  ( ( ph /\ x = B ) -> ( ps <-> ch ) )
4 iota2df.4 
 |-  F/ x ph
5 iota2df.5 
 |-  ( ph -> F/ x ch )
6 iota2df.6 
 |-  ( ph -> F/_ x B )
7 simpr 
 |-  ( ( ph /\ x = B ) -> x = B )
8 7 eqeq2d 
 |-  ( ( ph /\ x = B ) -> ( ( iota x ps ) = x <-> ( iota x ps ) = B ) )
9 3 8 bibi12d 
 |-  ( ( ph /\ x = B ) -> ( ( ps <-> ( iota x ps ) = x ) <-> ( ch <-> ( iota x ps ) = B ) ) )
10 iota1 
 |-  ( E! x ps -> ( ps <-> ( iota x ps ) = x ) )
11 2 10 syl 
 |-  ( ph -> ( ps <-> ( iota x ps ) = x ) )
12 nfiota1 
 |-  F/_ x ( iota x ps )
13 12 a1i 
 |-  ( ph -> F/_ x ( iota x ps ) )
14 13 6 nfeqd 
 |-  ( ph -> F/ x ( iota x ps ) = B )
15 5 14 nfbid 
 |-  ( ph -> F/ x ( ch <-> ( iota x ps ) = B ) )
16 1 9 11 4 6 15 vtocldf 
 |-  ( ph -> ( ch <-> ( iota x ps ) = B ) )