>>12157800>>12157844>are a function and its graph the exact same object"Yes."
But the issue with the question is that you're presuming set theoretical foundations apriori.
In that context, a function (or any other "object" for that matter) will be some set.
Two notes:
Firstly, By Extensionality, your function notion will forget about it's codomain.
E.g. let P(x,y) be y=x^3, let X=Y=N and let Y' be the union of N and the comlpex numbers.
Then with P, X,Y define the same function as X,Y'. That is to say, your notion of function e.g. has no inherent concept of surjection.
(Along the same line, there's then also a whole array of category theoretical notions that do the same job as epimorphisms, in Set)
You say
>a function f:XY is defined asbut "f:XY" here, if you play the set theory game in first order logic, is just some proposition about f.
Secondly (but that's just fyi), I just want to point out that while the definition is perfectly fine, there's the notion of class function that's not captured if, as you seem to do there, you require Y to be a set. E.g. ZF (unlike Z) has Replacement which enables you to map, via a predicate P, far out of the "comfort zone". E.g. you may want to "apply the powerset operation |N| times", and form the union of those sets, to get from the empty set to the infinite set of (hereditarily) finite sets. The function involved there isn't even a set but ZF don' care.
