Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Functions
fndmi
Next ⟩
fndmd
Metamath Proof Explorer
Ascii
Unicode
Theorem
fndmi
Description:
The domain of a function.
(Contributed by
Wolf Lammen
, 1-Jun-2024)
Ref
Expression
Hypothesis
fndmi.1
⊢
F
Fn
A
Assertion
fndmi
⊢
dom
⁡
F
=
A
Proof
Step
Hyp
Ref
Expression
1
fndmi.1
⊢
F
Fn
A
2
fndm
⊢
F
Fn
A
→
dom
⁡
F
=
A
3
1
2
ax-mp
⊢
dom
⁡
F
=
A