Theorem nexmo

Description: Nonexistence implies uniqueness. (Contributed by BJ, 30-Sep-2022) Avoid ax-11 . (Revised by Wolf Lammen, 16-Oct-2022)

	Ref	Expression
Assertion	nexmo	|- ( -. E. x ph -> E* x ph )

Proof

Step	Hyp	Ref	Expression
1		pm2.21	|- ( -. ph -> ( ph -> x = y ) )
2	1	alimi	|- ( A. x -. ph -> A. x ( ph -> x = y ) )
3	2	alrimiv	|- ( A. x -. ph -> A. y A. x ( ph -> x = y ) )
4	3	19.2d	|- ( A. x -. ph -> E. y A. x ( ph -> x = y ) )
5		alnex	|- ( A. x -. ph <-> -. E. x ph )
6	5	bicomi	|- ( -. E. x ph <-> A. x -. ph )
7		df-mo	|- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
8	4 6 7	3imtr4i	|- ( -. E. x ph -> E* x ph )