Theorem emptyex

Description: On the empty domain, any existentially quantified formula is false. (Contributed by Wolf Lammen, 21-Jan-2024)

	Ref	Expression
Assertion	emptyex	⊢ ( ¬ ∃ 𝑥 ⊤ → ¬ ∃ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		trud	⊢ ( 𝜑 → ⊤ )
2	1	eximi	⊢ ( ∃ 𝑥 𝜑 → ∃ 𝑥 ⊤ )
3	2	con3i	⊢ ( ¬ ∃ 𝑥 ⊤ → ¬ ∃ 𝑥 𝜑 )