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

Metamath Proof Explorer

Theorem eupickb

Description: Existential uniqueness "pick" showing wff equivalence. (Contributed by NM, 25-Nov-1994) (Proof shortened by Wolf Lammen, 27-Dec-2018)

Ref Expression
Assertion eupickb 
|- ( ( E! x ph /\ E! x ps /\ E. x ( ph /\ ps ) ) -> ( ph <-> ps ) )

Proof

Step Hyp Ref Expression
1 eupick 
 |-  ( ( E! x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )
2 1 3adant2 
 |-  ( ( E! x ph /\ E! x ps /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )
3 exancom 
 |-  ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
4 eupick 
 |-  ( ( E! x ps /\ E. x ( ps /\ ph ) ) -> ( ps -> ph ) )
5 3 4 sylan2b 
 |-  ( ( E! x ps /\ E. x ( ph /\ ps ) ) -> ( ps -> ph ) )
6 5 3adant1 
 |-  ( ( E! x ph /\ E! x ps /\ E. x ( ph /\ ps ) ) -> ( ps -> ph ) )
7 2 6 impbid 
 |-  ( ( E! x ph /\ E! x ps /\ E. x ( ph /\ ps ) ) -> ( ph <-> ps ) )