Theorem moeu2

Description: Uniqueness is equivalent to non-existence or unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by Peter Mazsa, 19-Nov-2024)

	Ref	Expression
Assertion	moeu2	|- ( E* x ph <-> ( -. E. x ph \/ E! x ph ) )

Proof

Step	Hyp	Ref	Expression
1		moeu	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
2		imor	|- ( ( E. x ph -> E! x ph ) <-> ( -. E. x ph \/ E! x ph ) )
3	1 2	bitri	|- ( E* x ph <-> ( -. E. x ph \/ E! x ph ) )