Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Functions
f0dom0
Next ⟩
f0rn0
Metamath Proof Explorer
Ascii
Unicode
Theorem
f0dom0
Description:
A function is empty iff it has an empty domain.
(Contributed by
AV
, 10-Feb-2019)
Ref
Expression
Assertion
f0dom0
⊢
F
:
X
⟶
Y
→
X
=
∅
↔
F
=
∅
Proof
Step
Hyp
Ref
Expression
1
feq2
⊢
X
=
∅
→
F
:
X
⟶
Y
↔
F
:
∅
⟶
Y
2
f0bi
⊢
F
:
∅
⟶
Y
↔
F
=
∅
3
2
biimpi
⊢
F
:
∅
⟶
Y
→
F
=
∅
4
1
3
syl6bi
⊢
X
=
∅
→
F
:
X
⟶
Y
→
F
=
∅
5
4
com12
⊢
F
:
X
⟶
Y
→
X
=
∅
→
F
=
∅
6
feq1
⊢
F
=
∅
→
F
:
X
⟶
Y
↔
∅
:
X
⟶
Y
7
dm0
⊢
dom
⁡
∅
=
∅
8
fdm
⊢
∅
:
X
⟶
Y
→
dom
⁡
∅
=
X
9
7
8
syl5reqr
⊢
∅
:
X
⟶
Y
→
X
=
∅
10
6
9
syl6bi
⊢
F
=
∅
→
F
:
X
⟶
Y
→
X
=
∅
11
10
com12
⊢
F
:
X
⟶
Y
→
F
=
∅
→
X
=
∅
12
5
11
impbid
⊢
F
:
X
⟶
Y
→
X
=
∅
↔
F
=
∅