Theorem n0moeu

Description: A case of equivalence of "at most one" and "only one". (Contributed by FL, 6-Dec-2010)

	Ref	Expression
Assertion	n0moeu	|- ( A =/= (/) -> ( E* x x e. A <-> E! x x e. A ) )

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( A =/= (/) <-> E. x x e. A )
2	1	biimpi	|- ( A =/= (/) -> E. x x e. A )
3	2	biantrurd	|- ( A =/= (/) -> ( E* x x e. A <-> ( E. x x e. A /\ E* x x e. A ) ) )
4		df-eu	|- ( E! x x e. A <-> ( E. x x e. A /\ E* x x e. A ) )
5	3 4	bitr4di	|- ( A =/= (/) -> ( E* x x e. A <-> E! x x e. A ) )