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

Metamath Proof Explorer

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 )