Metamath Proof Explorer

Theorem mob

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 mob 
|- ( ( ( A e. C /\ B e. D ) /\ E* x ph /\ ps ) -> ( A = B <-> ch ) )

Proof

Step Hyp Ref Expression
1 moi.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 moi.2 
 |-  ( x = B -> ( ph <-> ch ) )
3 elex 
 |-  ( B e. D -> B e. _V )
4 nfv 
 |-  F/ x B e. _V
5 nfmo1 
 |-  F/ x E* x ph
6 nfv 
 |-  F/ x ps
7 4 5 6 nf3an 
 |-  F/ x ( B e. _V /\ E* x ph /\ ps )
8 nfv 
 |-  F/ x ( A = B <-> ch )
9 7 8 nfim 
 |-  F/ x ( ( B e. _V /\ E* x ph /\ ps ) -> ( A = B <-> ch ) )
10 1 3anbi3d 
 |-  ( x = A -> ( ( B e. _V /\ E* x ph /\ ph ) <-> ( B e. _V /\ E* x ph /\ ps ) ) )
11 eqeq1 
 |-  ( x = A -> ( x = B <-> A = B ) )
12 11 bibi1d 
 |-  ( x = A -> ( ( x = B <-> ch ) <-> ( A = B <-> ch ) ) )
13 10 12 imbi12d 
 |-  ( x = A -> ( ( ( B e. _V /\ E* x ph /\ ph ) -> ( x = B <-> ch ) ) <-> ( ( B e. _V /\ E* x ph /\ ps ) -> ( A = B <-> ch ) ) ) )
14 2 mob2 
 |-  ( ( B e. _V /\ E* x ph /\ ph ) -> ( x = B <-> ch ) )
15 9 13 14 vtoclg1f 
 |-  ( A e. C -> ( ( B e. _V /\ E* x ph /\ ps ) -> ( A = B <-> ch ) ) )
16 15 com12 
 |-  ( ( B e. _V /\ E* x ph /\ ps ) -> ( A e. C -> ( A = B <-> ch ) ) )
17 16 3expib 
 |-  ( B e. _V -> ( ( E* x ph /\ ps ) -> ( A e. C -> ( A = B <-> ch ) ) ) )
18 3 17 syl 
 |-  ( B e. D -> ( ( E* x ph /\ ps ) -> ( A e. C -> ( A = B <-> ch ) ) ) )
19 18 com3r 
 |-  ( A e. C -> ( B e. D -> ( ( E* x ph /\ ps ) -> ( A = B <-> ch ) ) ) )
20 19 imp 
 |-  ( ( A e. C /\ B e. D ) -> ( ( E* x ph /\ ps ) -> ( A = B <-> ch ) ) )
21 20 3impib 
 |-  ( ( ( A e. C /\ B e. D ) /\ E* x ph /\ ps ) -> ( A = B <-> ch ) )