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

Metamath Proof Explorer

Theorem reupick3

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

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

Proof

Step Hyp Ref Expression
1 df-reu 
 |-  ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
2 df-rex 
 |-  ( E. x e. A ( ph /\ ps ) <-> E. x ( x e. A /\ ( ph /\ ps ) ) )
3 anass 
 |-  ( ( ( x e. A /\ ph ) /\ ps ) <-> ( x e. A /\ ( ph /\ ps ) ) )
4 3 exbii 
 |-  ( E. x ( ( x e. A /\ ph ) /\ ps ) <-> E. x ( x e. A /\ ( ph /\ ps ) ) )
5 2 4 bitr4i 
 |-  ( E. x e. A ( ph /\ ps ) <-> E. x ( ( x e. A /\ ph ) /\ ps ) )
6 eupick 
 |-  ( ( E! x ( x e. A /\ ph ) /\ E. x ( ( x e. A /\ ph ) /\ ps ) ) -> ( ( x e. A /\ ph ) -> ps ) )
7 1 5 6 syl2anb 
 |-  ( ( E! x e. A ph /\ E. x e. A ( ph /\ ps ) ) -> ( ( x e. A /\ ph ) -> ps ) )
8 7 expd 
 |-  ( ( E! x e. A ph /\ E. x e. A ( ph /\ ps ) ) -> ( x e. A -> ( ph -> ps ) ) )
9 8 3impia 
 |-  ( ( E! x e. A ph /\ E. x e. A ( ph /\ ps ) /\ x e. A ) -> ( ph -> ps ) )