Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
moel
Next ⟩
mormo
Metamath Proof Explorer
Ascii
Unicode
Theorem
moel
Description:
"At most one" element in a set.
(Contributed by
Thierry Arnoux
, 26-Jul-2018)
Ref
Expression
Assertion
moel
⊢
∃
*
x
x
∈
A
↔
∀
x
∈
A
∀
y
∈
A
x
=
y
Proof
Step
Hyp
Ref
Expression
1
ralcom4
⊢
∀
x
∈
A
∀
y
y
∈
A
→
x
=
y
↔
∀
y
∀
x
∈
A
y
∈
A
→
x
=
y
2
df-ral
⊢
∀
y
∈
A
x
=
y
↔
∀
y
y
∈
A
→
x
=
y
3
2
ralbii
⊢
∀
x
∈
A
∀
y
∈
A
x
=
y
↔
∀
x
∈
A
∀
y
y
∈
A
→
x
=
y
4
alcom
⊢
∀
x
∀
y
x
∈
A
∧
y
∈
A
→
x
=
y
↔
∀
y
∀
x
x
∈
A
∧
y
∈
A
→
x
=
y
5
eleq1w
⊢
x
=
y
→
x
∈
A
↔
y
∈
A
6
5
mo4
⊢
∃
*
x
x
∈
A
↔
∀
x
∀
y
x
∈
A
∧
y
∈
A
→
x
=
y
7
df-ral
⊢
∀
x
∈
A
y
∈
A
→
x
=
y
↔
∀
x
x
∈
A
→
y
∈
A
→
x
=
y
8
impexp
⊢
x
∈
A
∧
y
∈
A
→
x
=
y
↔
x
∈
A
→
y
∈
A
→
x
=
y
9
8
albii
⊢
∀
x
x
∈
A
∧
y
∈
A
→
x
=
y
↔
∀
x
x
∈
A
→
y
∈
A
→
x
=
y
10
7
9
bitr4i
⊢
∀
x
∈
A
y
∈
A
→
x
=
y
↔
∀
x
x
∈
A
∧
y
∈
A
→
x
=
y
11
10
albii
⊢
∀
y
∀
x
∈
A
y
∈
A
→
x
=
y
↔
∀
y
∀
x
x
∈
A
∧
y
∈
A
→
x
=
y
12
4
6
11
3bitr4i
⊢
∃
*
x
x
∈
A
↔
∀
y
∀
x
∈
A
y
∈
A
→
x
=
y
13
1
3
12
3bitr4ri
⊢
∃
*
x
x
∈
A
↔
∀
x
∈
A
∀
y
∈
A
x
=
y