Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The universal class
mo2icl
Next ⟩
mob2
Metamath Proof Explorer
Ascii
Unicode
Theorem
mo2icl
Description:
Theorem for inferring "at most one."
(Contributed by
NM
, 17-Oct-1996)
Ref
Expression
Assertion
mo2icl
⊢
∀
x
φ
→
x
=
A
→
∃
*
x
φ
Proof
Step
Hyp
Ref
Expression
1
eqeq2
⊢
y
=
A
→
x
=
y
↔
x
=
A
2
1
imbi2d
⊢
y
=
A
→
φ
→
x
=
y
↔
φ
→
x
=
A
3
2
albidv
⊢
y
=
A
→
∀
x
φ
→
x
=
y
↔
∀
x
φ
→
x
=
A
4
3
imbi1d
⊢
y
=
A
→
∀
x
φ
→
x
=
y
→
∃
*
x
φ
↔
∀
x
φ
→
x
=
A
→
∃
*
x
φ
5
19.8a
⊢
∀
x
φ
→
x
=
y
→
∃
y
∀
x
φ
→
x
=
y
6
df-mo
⊢
∃
*
x
φ
↔
∃
y
∀
x
φ
→
x
=
y
7
5
6
sylibr
⊢
∀
x
φ
→
x
=
y
→
∃
*
x
φ
8
4
7
vtoclg
⊢
A
∈
V
→
∀
x
φ
→
x
=
A
→
∃
*
x
φ
9
eqvisset
⊢
x
=
A
→
A
∈
V
10
9
imim2i
⊢
φ
→
x
=
A
→
φ
→
A
∈
V
11
10
con3rr3
⊢
¬
A
∈
V
→
φ
→
x
=
A
→
¬
φ
12
11
alimdv
⊢
¬
A
∈
V
→
∀
x
φ
→
x
=
A
→
∀
x
¬
φ
13
alnex
⊢
∀
x
¬
φ
↔
¬
∃
x
φ
14
nexmo
⊢
¬
∃
x
φ
→
∃
*
x
φ
15
13
14
sylbi
⊢
∀
x
¬
φ
→
∃
*
x
φ
16
12
15
syl6
⊢
¬
A
∈
V
→
∀
x
φ
→
x
=
A
→
∃
*
x
φ
17
8
16
pm2.61i
⊢
∀
x
φ
→
x
=
A
→
∃
*
x
φ