Theorem moi2

Description: Consequence of "at most one." (Contributed by NM, 29-Jun-2008)

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

Proof

Step	Hyp	Ref	Expression
1		moi2.1	|- ( x = A -> ( ph <-> ps ) )
2	1	mob2	|- ( ( A e. B /\ E* x ph /\ ph ) -> ( x = A <-> ps ) )
3	2	3expa	|- ( ( ( A e. B /\ E* x ph ) /\ ph ) -> ( x = A <-> ps ) )
4	3	biimprd	|- ( ( ( A e. B /\ E* x ph ) /\ ph ) -> ( ps -> x = A ) )
5	4	impr	|- ( ( ( A e. B /\ E* x ph ) /\ ( ph /\ ps ) ) -> x = A )