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 ) )