Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The empty set
eq0rdv
Next ⟩
csbprc
Metamath Proof Explorer
Ascii
Unicode
Theorem
eq0rdv
Description:
Deduction for equality to the empty set.
(Contributed by
NM
, 11-Jul-2014)
Ref
Expression
Hypothesis
eq0rdv.1
⊢
φ
→
¬
x
∈
A
Assertion
eq0rdv
⊢
φ
→
A
=
∅
Proof
Step
Hyp
Ref
Expression
1
eq0rdv.1
⊢
φ
→
¬
x
∈
A
2
1
pm2.21d
⊢
φ
→
x
∈
A
→
x
∈
∅
3
2
ssrdv
⊢
φ
→
A
⊆
∅
4
ss0
⊢
A
⊆
∅
→
A
=
∅
5
3
4
syl
⊢
φ
→
A
=
∅