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

Metamath Proof Explorer

Theorem morex

Description: Derive membership from uniqueness. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses morex.1 
|- B e. _V
morex.2 
|- ( x = B -> ( ph <-> ps ) )
Assertion morex 
|- ( ( E. x e. A ph /\ E* x ph ) -> ( ps -> B e. A ) )

Proof

Step Hyp Ref Expression
1 morex.1 
 |-  B e. _V
2 morex.2 
 |-  ( x = B -> ( ph <-> ps ) )
3 df-rex 
 |-  ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4 exancom 
 |-  ( E. x ( x e. A /\ ph ) <-> E. x ( ph /\ x e. A ) )
5 3 4 bitri 
 |-  ( E. x e. A ph <-> E. x ( ph /\ x e. A ) )
6 nfmo1 
 |-  F/ x E* x ph
7 nfe1 
 |-  F/ x E. x ( ph /\ x e. A )
8 6 7 nfan 
 |-  F/ x ( E* x ph /\ E. x ( ph /\ x e. A ) )
9 mopick 
 |-  ( ( E* x ph /\ E. x ( ph /\ x e. A ) ) -> ( ph -> x e. A ) )
10 8 9 alrimi 
 |-  ( ( E* x ph /\ E. x ( ph /\ x e. A ) ) -> A. x ( ph -> x e. A ) )
11 eleq1 
 |-  ( x = B -> ( x e. A <-> B e. A ) )
12 2 11 imbi12d 
 |-  ( x = B -> ( ( ph -> x e. A ) <-> ( ps -> B e. A ) ) )
13 1 12 spcv 
 |-  ( A. x ( ph -> x e. A ) -> ( ps -> B e. A ) )
14 10 13 syl 
 |-  ( ( E* x ph /\ E. x ( ph /\ x e. A ) ) -> ( ps -> B e. A ) )
15 5 14 sylan2b 
 |-  ( ( E* x ph /\ E. x e. A ph ) -> ( ps -> B e. A ) )
16 15 ancoms 
 |-  ( ( E. x e. A ph /\ E* x ph ) -> ( ps -> B e. A ) )