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	⊢ ( ∀ 𝑥 𝜑 → ¬ ∃! 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		eunex	⊢ ( ∃! 𝑥 𝜑 → ∃ 𝑥 ¬ 𝜑 )
2		exnal	⊢ ( ∃ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑥 𝜑 )
3	1 2	sylib	⊢ ( ∃! 𝑥 𝜑 → ¬ ∀ 𝑥 𝜑 )
4	3	con2i	⊢ ( ∀ 𝑥 𝜑 → ¬ ∃! 𝑥 𝜑 )