Theorem nmo

Description: Negation of "at most one". (Contributed by Thierry Arnoux, 26-Feb-2017)

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

Proof

Step	Hyp	Ref	Expression
1		nmo.1	|- F/ y ph
2	1	mof	|- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
3	2	notbii	|- ( -. E* x ph <-> -. E. y A. x ( ph -> x = y ) )
4		alnex	|- ( A. y -. A. x ( ph -> x = y ) <-> -. E. y A. x ( ph -> x = y ) )
5		exnal	|- ( E. x -. ( ph -> x = y ) <-> -. A. x ( ph -> x = y ) )
6		pm4.61	|- ( -. ( ph -> x = y ) <-> ( ph /\ -. x = y ) )
7		biid	|- ( x = y <-> x = y )
8	7	necon3bbii	|- ( -. x = y <-> x =/= y )
9	8	anbi2i	|- ( ( ph /\ -. x = y ) <-> ( ph /\ x =/= y ) )
10	6 9	bitri	|- ( -. ( ph -> x = y ) <-> ( ph /\ x =/= y ) )
11	10	exbii	|- ( E. x -. ( ph -> x = y ) <-> E. x ( ph /\ x =/= y ) )
12	5 11	bitr3i	|- ( -. A. x ( ph -> x = y ) <-> E. x ( ph /\ x =/= y ) )
13	12	albii	|- ( A. y -. A. x ( ph -> x = y ) <-> A. y E. x ( ph /\ x =/= y ) )
14	3 4 13	3bitr2i	|- ( -. E* x ph <-> A. y E. x ( ph /\ x =/= y ) )