Metamath Proof Explorer

Theorem rmob

Description: Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015) (Revised by NM, 16-Jun-2017)

Ref Expression
Hypotheses rmoi.b 
|- ( x = B -> ( ph <-> ps ) )
rmoi.c 
|- ( x = C -> ( ph <-> ch ) )
Assertion rmob 
|- ( ( E* x e. A ph /\ ( B e. A /\ ps ) ) -> ( B = C <-> ( C e. A /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 rmoi.b 
 |-  ( x = B -> ( ph <-> ps ) )
2 rmoi.c 
 |-  ( x = C -> ( ph <-> ch ) )
3 df-rmo 
 |-  ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
4 simprl 
 |-  ( ( E* x ( x e. A /\ ph ) /\ ( B e. A /\ ps ) ) -> B e. A )
5 eleq1 
 |-  ( B = C -> ( B e. A <-> C e. A ) )
6 4 5 syl5ibcom 
 |-  ( ( E* x ( x e. A /\ ph ) /\ ( B e. A /\ ps ) ) -> ( B = C -> C e. A ) )
7 simpl 
 |-  ( ( C e. A /\ ch ) -> C e. A )
8 7 a1i 
 |-  ( ( E* x ( x e. A /\ ph ) /\ ( B e. A /\ ps ) ) -> ( ( C e. A /\ ch ) -> C e. A ) )
9 4 anim1i 
 |-  ( ( ( E* x ( x e. A /\ ph ) /\ ( B e. A /\ ps ) ) /\ C e. A ) -> ( B e. A /\ C e. A ) )
10 simpll 
 |-  ( ( ( E* x ( x e. A /\ ph ) /\ ( B e. A /\ ps ) ) /\ C e. A ) -> E* x ( x e. A /\ ph ) )
11 simplr 
 |-  ( ( ( E* x ( x e. A /\ ph ) /\ ( B e. A /\ ps ) ) /\ C e. A ) -> ( B e. A /\ ps ) )
12 eleq1 
 |-  ( x = B -> ( x e. A <-> B e. A ) )
13 12 1 anbi12d 
 |-  ( x = B -> ( ( x e. A /\ ph ) <-> ( B e. A /\ ps ) ) )
14 eleq1 
 |-  ( x = C -> ( x e. A <-> C e. A ) )
15 14 2 anbi12d 
 |-  ( x = C -> ( ( x e. A /\ ph ) <-> ( C e. A /\ ch ) ) )
16 13 15 mob 
 |-  ( ( ( B e. A /\ C e. A ) /\ E* x ( x e. A /\ ph ) /\ ( B e. A /\ ps ) ) -> ( B = C <-> ( C e. A /\ ch ) ) )
17 9 10 11 16 syl3anc 
 |-  ( ( ( E* x ( x e. A /\ ph ) /\ ( B e. A /\ ps ) ) /\ C e. A ) -> ( B = C <-> ( C e. A /\ ch ) ) )
18 17 ex 
 |-  ( ( E* x ( x e. A /\ ph ) /\ ( B e. A /\ ps ) ) -> ( C e. A -> ( B = C <-> ( C e. A /\ ch ) ) ) )
19 6 8 18 pm5.21ndd 
 |-  ( ( E* x ( x e. A /\ ph ) /\ ( B e. A /\ ps ) ) -> ( B = C <-> ( C e. A /\ ch ) ) )
20 3 19 sylanb 
 |-  ( ( E* x e. A ph /\ ( B e. A /\ ps ) ) -> ( B = C <-> ( C e. A /\ ch ) ) )