Thats not the correct approach in logic. Since Peano, we find something else:
"Function application. "(𝐹‘𝑥)" should be read "the value of function 𝐹 at 𝑥" and
has the same meaning as the more familiar but ambiguous notation F(x).
For example, (cos‘0) = 1 (see cos0 14824). The left apostrophe notation
originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell]
p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26.
See df-fv 5865. In the ASCII (input) representation there are spaces around the
grave accent; there is a single accent when it is used directly, and it is
doubled within comments."
http://us.metamath.org/mpeuni/conventions.html
Metamath can use the same symbol for function F and the function graph F,
in the above F is the same referent. Metamath uses then the empty set as
undefined marker, in case an argument is not in dom(F).
There are even aspects of definite description, F need not be a function graph
per see. They can therefore prove the following definite descriptions theorem.
It is not like in Russell, where we get false, its more we get the defined marker:
/* Provable in Metamath */
~ EXISTUNIQUE(x) (a,x) e F => (F'a) = {}
I don't think DC Proof/Donnie Darko has such a maker u:
/* Not Provable in DC Proof with Donnie Darke Function approach */
~ EXISTUNIQUE(x) (a,x) e F => F(a) = u
The Peano apostroph was later adopted by for example Withhead Russell,
Quine, Takeuti Zaring. It only needs some set theory like ZFC. So yes, DC
Proof with Donnie Darke Function approach is not what is common in logic.