Metamath Proof Explorer


Theorem fndm

Description: The domain of a function. (Contributed by NM, 2-Aug-1994)

Ref Expression
Assertion fndm FFnAdomF=A

Proof

Step Hyp Ref Expression
1 df-fn FFnAFunFdomF=A
2 1 simprbi FFnAdomF=A