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 ) )