Metamath Proof Explorer
Description: There does not exist at most one set such that T. is true.
(Contributed by Anthony Hart, 13-Sep-2011)
|
|
Ref |
Expression |
|
Assertion |
nmotru |
⊢ ¬ ∃* 𝑥 ⊤ |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
extru |
⊢ ∃ 𝑥 ⊤ |
2 |
|
neutru |
⊢ ¬ ∃! 𝑥 ⊤ |
3 |
|
jcn |
⊢ ( ∃ 𝑥 ⊤ → ( ¬ ∃! 𝑥 ⊤ → ¬ ( ∃ 𝑥 ⊤ → ∃! 𝑥 ⊤ ) ) ) |
4 |
1 2 3
|
mp2 |
⊢ ¬ ( ∃ 𝑥 ⊤ → ∃! 𝑥 ⊤ ) |
5 |
|
moeu |
⊢ ( ∃* 𝑥 ⊤ ↔ ( ∃ 𝑥 ⊤ → ∃! 𝑥 ⊤ ) ) |
6 |
4 5
|
mtbir |
⊢ ¬ ∃* 𝑥 ⊤ |