Theorem mo

Description: Equivalent definitions of "there exists at most one". (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 2-Dec-2018)

	Ref	Expression
Hypothesis	mo.nf	|- F/ y ph
Assertion	mo	|- ( E. y A. x ( ph -> x = y ) <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )

Proof

Step	Hyp	Ref	Expression
1		mo.nf	|- F/ y ph
2	1	mof	|- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
3	1	mo3	|- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
4	2 3	bitr3i	|- ( E. y A. x ( ph -> x = y ) <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )