I am convinced that the following is true, I just need to double check myself, and also maybe share this with a community, since I find it beautiful.(if it is true)
Let us consider "the standard foundations of mathematics" the first order set theory ZFC.
It has model that using partial functions: (see article WILLIAM M. FARMER, JOSHUA D. GUTTMAN: A Set Theory with Support for Partial Functions )
Let's define value of the function the following way: $"f(x)" := (\iota y: \langle x,y\rangle \in f)$ (here $f$ and $x$ are object variables, and iota is THE definite description operator :) ).
Without a doubt, the following sequence is valid:
$(\langle x,y\rangle \in f) \Rightarrow (f(x)=y)$
My claim is that the opposite implication is also valid:
$(f(x)=y) \Rightarrow (\langle x,y\rangle \in f)$
Because
- if $x\in \mbox{dom}(f)$(don't pay attention to parenthesis here: it can be rewritten) is true under fixed interpretation and fixed evaluation of object variables then it is true implication.
- if it is not, then (f(x)=y) is automatically a false formula under fixed interpretation and evaluation. (This claim is based on interpretation with partial functions, described in the article.) Therefore the implication is still true, as if it was "$\mbox{false}\Rightarrow \varphi$".
So the following formula/sequence is valid: $(f(x)=y) \Leftrightarrow (\langle x,y\rangle \in f)$ and we can substitute one side of the equivalence with the other voluntarily in other proofs, without any need for any precautions.
Is everything correct?