Theorem rmo2

Description: Alternate definition of restricted "at most one". Note that E* x e. A ph is not equivalent to E. y e. A A. x e. A ( ph -> x = y ) (in analogy to reu6 ); to see this, let A be the empty set. However, one direction of this pattern holds; see rmo2i . (Contributed by NM, 17-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		rmo2.1	|- F/ y ph
2		df-rmo	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
3		nfv	|- F/ y x e. A
4	3 1	nfan	|- F/ y ( x e. A /\ ph )
5	4	mof	|- ( E* x ( x e. A /\ ph ) <-> E. y A. x ( ( x e. A /\ ph ) -> x = y ) )
6		impexp	|- ( ( ( x e. A /\ ph ) -> x = y ) <-> ( x e. A -> ( ph -> x = y ) ) )
7	6	albii	|- ( A. x ( ( x e. A /\ ph ) -> x = y ) <-> A. x ( x e. A -> ( ph -> x = y ) ) )
8		df-ral	|- ( A. x e. A ( ph -> x = y ) <-> A. x ( x e. A -> ( ph -> x = y ) ) )
9	7 8	bitr4i	|- ( A. x ( ( x e. A /\ ph ) -> x = y ) <-> A. x e. A ( ph -> x = y ) )
10	9	exbii	|- ( E. y A. x ( ( x e. A /\ ph ) -> x = y ) <-> E. y A. x e. A ( ph -> x = y ) )
11	2 5 10	3bitri	|- ( E* x e. A ph <-> E. y A. x e. A ( ph -> x = y ) )