This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
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 |
⊢ ( 𝐴 = ∅ → ∃* 𝑥 𝑥 ∈ 𝐴 ) |