Theorem mob2

Description: Consequence of "at most one". (Contributed by NM, 2-Jan-2015)

	Ref	Expression
Hypothesis	moi2.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	mob2	|- ( ( A e. B /\ E* x ph /\ ph ) -> ( x = A <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		moi2.1	|- ( x = A -> ( ph <-> ps ) )
2		simp3	|- ( ( A e. B /\ E* x ph /\ ph ) -> ph )
3	2 1	syl5ibcom	|- ( ( A e. B /\ E* x ph /\ ph ) -> ( x = A -> ps ) )
4		nfv	|- F/ x ps
5	4 1	sbhypf	|- ( y = A -> ( [ y / x ] ph <-> ps ) )
6	5	anbi2d	|- ( y = A -> ( ( ph /\ [ y / x ] ph ) <-> ( ph /\ ps ) ) )
7		eqeq2	|- ( y = A -> ( x = y <-> x = A ) )
8	6 7	imbi12d	|- ( y = A -> ( ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> ( ( ph /\ ps ) -> x = A ) ) )
9	8	spcgv	|- ( A e. B -> ( A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( ( ph /\ ps ) -> x = A ) ) )
10		nfs1v	|- F/ x [ y / x ] ph
11		sbequ12	|- ( x = y -> ( ph <-> [ y / x ] ph ) )
12	10 11	mo4f	|- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
13		sp	|- ( A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) -> A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
14	12 13	sylbi	|- ( E* x ph -> A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
15	9 14	impel	|- ( ( A e. B /\ E* x ph ) -> ( ( ph /\ ps ) -> x = A ) )
16	15	expd	|- ( ( A e. B /\ E* x ph ) -> ( ph -> ( ps -> x = A ) ) )
17	16	3impia	|- ( ( A e. B /\ E* x ph /\ ph ) -> ( ps -> x = A ) )
18	3 17	impbid	|- ( ( A e. B /\ E* x ph /\ ph ) -> ( x = A <-> ps ) )