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

Metamath Proof Explorer

Theorem pm14.24

Description: Theorem *14.24 in WhiteheadRussell p. 191. (Contributed by Andrew Salmon, 12-Jul-2011)

Ref Expression
Assertion pm14.24 
|- ( E! x ph -> A. y ( [. y / x ]. ph <-> y = ( iota x ph ) ) )

Proof

Step Hyp Ref Expression
1 nfeu1 
 |-  F/ x E! x ph
2 nfsbc1v 
 |-  F/ x [. y / x ]. ph
3 pm14.12 
 |-  ( E! x ph -> A. x A. y ( ( ph /\ [. y / x ]. ph ) -> x = y ) )
4 3 19.21bbi 
 |-  ( E! x ph -> ( ( ph /\ [. y / x ]. ph ) -> x = y ) )
5 4 ancomsd 
 |-  ( E! x ph -> ( ( [. y / x ]. ph /\ ph ) -> x = y ) )
6 5 expdimp 
 |-  ( ( E! x ph /\ [. y / x ]. ph ) -> ( ph -> x = y ) )
7 pm13.13b 
 |-  ( ( [. y / x ]. ph /\ x = y ) -> ph )
8 7 ex 
 |-  ( [. y / x ]. ph -> ( x = y -> ph ) )
9 8 adantl 
 |-  ( ( E! x ph /\ [. y / x ]. ph ) -> ( x = y -> ph ) )
10 6 9 impbid 
 |-  ( ( E! x ph /\ [. y / x ]. ph ) -> ( ph <-> x = y ) )
11 10 ex 
 |-  ( E! x ph -> ( [. y / x ]. ph -> ( ph <-> x = y ) ) )
12 1 2 11 alrimd 
 |-  ( E! x ph -> ( [. y / x ]. ph -> A. x ( ph <-> x = y ) ) )
13 iotaval 
 |-  ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )
14 13 eqcomd 
 |-  ( A. x ( ph <-> x = y ) -> y = ( iota x ph ) )
15 12 14 syl6 
 |-  ( E! x ph -> ( [. y / x ]. ph -> y = ( iota x ph ) ) )
16 iota4 
 |-  ( E! x ph -> [. ( iota x ph ) / x ]. ph )
17 dfsbcq 
 |-  ( y = ( iota x ph ) -> ( [. y / x ]. ph <-> [. ( iota x ph ) / x ]. ph ) )
18 16 17 syl5ibrcom 
 |-  ( E! x ph -> ( y = ( iota x ph ) -> [. y / x ]. ph ) )
19 15 18 impbid 
 |-  ( E! x ph -> ( [. y / x ]. ph <-> y = ( iota x ph ) ) )
20 19 alrimiv 
 |-  ( E! x ph -> A. y ( [. y / x ]. ph <-> y = ( iota x ph ) ) )