Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
General Observations
eu0
Next ⟩
epelon2
Metamath Proof Explorer
Ascii
Unicode
Theorem
eu0
Description:
There is only one empty set.
(Contributed by
RP
, 1-Oct-2023)
Ref
Expression
Assertion
eu0
⊢
∀
x
¬
x
∈
∅
∧
∃!
x
∀
y
¬
y
∈
x
Proof
Step
Hyp
Ref
Expression
1
noel
⊢
¬
x
∈
∅
2
1
ax-gen
⊢
∀
x
¬
x
∈
∅
3
ax-nul
⊢
∃
x
∀
y
¬
y
∈
x
4
nulmo
⊢
∃
*
x
∀
y
¬
y
∈
x
5
df-eu
⊢
∃!
x
∀
y
¬
y
∈
x
↔
∃
x
∀
y
¬
y
∈
x
∧
∃
*
x
∀
y
¬
y
∈
x
6
3
4
5
mpbir2an
⊢
∃!
x
∀
y
¬
y
∈
x
7
2
6
pm3.2i
⊢
∀
x
¬
x
∈
∅
∧
∃!
x
∀
y
¬
y
∈
x