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

Metamath Proof Explorer

Theorem rmob2

Description: Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019)

Ref Expression
Hypotheses rmoi2.1 
|- ( x = B -> ( ps <-> ch ) )
rmoi2.2 
|- ( ph -> B e. A )
rmoi2.3 
|- ( ph -> E* x e. A ps )
rmoi2.4 
|- ( ph -> x e. A )
rmoi2.5 
|- ( ph -> ps )
Assertion rmob2 
|- ( ph -> ( x = B <-> ch ) )

Proof

Step Hyp Ref Expression
1 rmoi2.1 
 |-  ( x = B -> ( ps <-> ch ) )
2 rmoi2.2 
 |-  ( ph -> B e. A )
3 rmoi2.3 
 |-  ( ph -> E* x e. A ps )
4 rmoi2.4 
 |-  ( ph -> x e. A )
5 rmoi2.5 
 |-  ( ph -> ps )
6 df-rmo 
 |-  ( E* x e. A ps <-> E* x ( x e. A /\ ps ) )
7 3 6 sylib 
 |-  ( ph -> E* x ( x e. A /\ ps ) )
8 eleq1 
 |-  ( x = B -> ( x e. A <-> B e. A ) )
9 8 1 anbi12d 
 |-  ( x = B -> ( ( x e. A /\ ps ) <-> ( B e. A /\ ch ) ) )
10 9 mob2 
 |-  ( ( B e. A /\ E* x ( x e. A /\ ps ) /\ ( x e. A /\ ps ) ) -> ( x = B <-> ( B e. A /\ ch ) ) )
11 2 7 4 5 10 syl112anc 
 |-  ( ph -> ( x = B <-> ( B e. A /\ ch ) ) )
12 2 11 mpbirand 
 |-  ( ph -> ( x = B <-> ch ) )