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

Metamath Proof Explorer

Theorem reupick2

Description: Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 15-Dec-2013) (Proof shortened by Mario Carneiro, 19-Nov-2016)

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

Proof

Step Hyp Ref Expression
1 ancr 
 |-  ( ( ps -> ph ) -> ( ps -> ( ph /\ ps ) ) )
2 1 ralimi 
 |-  ( A. x e. A ( ps -> ph ) -> A. x e. A ( ps -> ( ph /\ ps ) ) )
3 rexim 
 |-  ( A. x e. A ( ps -> ( ph /\ ps ) ) -> ( E. x e. A ps -> E. x e. A ( ph /\ ps ) ) )
4 2 3 syl 
 |-  ( A. x e. A ( ps -> ph ) -> ( E. x e. A ps -> E. x e. A ( ph /\ ps ) ) )
5 reupick3 
 |-  ( ( E! x e. A ph /\ E. x e. A ( ph /\ ps ) /\ x e. A ) -> ( ph -> ps ) )
6 5 3exp 
 |-  ( E! x e. A ph -> ( E. x e. A ( ph /\ ps ) -> ( x e. A -> ( ph -> ps ) ) ) )
7 6 com12 
 |-  ( E. x e. A ( ph /\ ps ) -> ( E! x e. A ph -> ( x e. A -> ( ph -> ps ) ) ) )
8 4 7 syl6 
 |-  ( A. x e. A ( ps -> ph ) -> ( E. x e. A ps -> ( E! x e. A ph -> ( x e. A -> ( ph -> ps ) ) ) ) )
9 8 3imp1 
 |-  ( ( ( A. x e. A ( ps -> ph ) /\ E. x e. A ps /\ E! x e. A ph ) /\ x e. A ) -> ( ph -> ps ) )
10 rsp 
 |-  ( A. x e. A ( ps -> ph ) -> ( x e. A -> ( ps -> ph ) ) )
11 10 3ad2ant1 
 |-  ( ( A. x e. A ( ps -> ph ) /\ E. x e. A ps /\ E! x e. A ph ) -> ( x e. A -> ( ps -> ph ) ) )
12 11 imp 
 |-  ( ( ( A. x e. A ( ps -> ph ) /\ E. x e. A ps /\ E! x e. A ph ) /\ x e. A ) -> ( ps -> ph ) )
13 9 12 impbid 
 |-  ( ( ( A. x e. A ( ps -> ph ) /\ E. x e. A ps /\ E! x e. A ph ) /\ x e. A ) -> ( ph <-> ps ) )