Theorem mo0

Description: "At most one" element in an empty set. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mo0	⊢ ( 𝐴 = ∅ → ∃* 𝑥 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		vsn	⊢ { V } = ∅
2	1	eqcomi	⊢ ∅ = { V }
3		eqeq1	⊢ ( 𝐴 = ∅ → ( 𝐴 = { V } ↔ ∅ = { V } ) )
4	2 3	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 = { V } )
5		mosn	⊢ ( 𝐴 = { V } → ∃* 𝑥 𝑥 ∈ 𝐴 )
6	4 5	syl	⊢ ( 𝐴 = ∅ → ∃* 𝑥 𝑥 ∈ 𝐴 )