Theorem rmo2i

Description: Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017)

	Ref	Expression
Hypothesis	rmo2.1	|- F/ y ph
Assertion	rmo2i	|- ( E. y e. A A. x e. A ( ph -> x = y ) -> E* x e. A ph )

Proof

Step	Hyp	Ref	Expression
1		rmo2.1	|- F/ y ph
2		rexex	|- ( E. y e. A A. x e. A ( ph -> x = y ) -> E. y A. x e. A ( ph -> x = y ) )
3	1	rmo2	|- ( E* x e. A ph <-> E. y A. x e. A ( ph -> x = y ) )
4	2 3	sylibr	|- ( E. y e. A A. x e. A ( ph -> x = y ) -> E* x e. A ph )