Theorem rmoi2

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 )
	rmoi2.6	|- ( ph -> ch )
Assertion	rmoi2	|- ( ph -> x = B )

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		rmoi2.6	|- ( ph -> ch )
7	1 2 3 4 5	rmob2	|- ( ph -> ( x = B <-> ch ) )
8	6 7	mpbird	|- ( ph -> x = B )