Metamath Proof Explorer


Theorem iota2df

Description: A condition that allows us 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 ) )