Theorem moi

Description: Equality implied by "at most one". (Contributed by NM, 18-Feb-2006)

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

Proof

Step	Hyp	Ref	Expression
1		moi.1	|- ( x = A -> ( ph <-> ps ) )
2		moi.2	|- ( x = B -> ( ph <-> ch ) )
3	1 2	mob	|- ( ( ( A e. C /\ B e. D ) /\ E* x ph /\ ps ) -> ( A = B <-> ch ) )
4	3	biimprd	|- ( ( ( A e. C /\ B e. D ) /\ E* x ph /\ ps ) -> ( ch -> A = B ) )
5	4	3expia	|- ( ( ( A e. C /\ B e. D ) /\ E* x ph ) -> ( ps -> ( ch -> A = B ) ) )
6	5	impd	|- ( ( ( A e. C /\ B e. D ) /\ E* x ph ) -> ( ( ps /\ ch ) -> A = B ) )
7	6	3impia	|- ( ( ( A e. C /\ B e. D ) /\ E* x ph /\ ( ps /\ ch ) ) -> A = B )