Theorem alneu

Description: If a statement holds for all sets, there is not a unique set for which the statement holds. (Contributed by Alexander van der Vekens, 28-Nov-2017)

	Ref	Expression
Assertion	alneu	|- ( A. x ph -> -. E! x ph )

Proof

Step	Hyp	Ref	Expression
1		eunex	|- ( E! x ph -> E. x -. ph )
2		exnal	|- ( E. x -. ph <-> -. A. x ph )
3	1 2	sylib	|- ( E! x ph -> -. A. x ph )
4	3	con2i	|- ( A. x ph -> -. E! x ph )