Basic question on function mapping and FOL

Question

Let the sets $X=\{1,2\}$ and $Y=\{2,3\}$. Let $[1 \in X \rightarrow 2 \in Y] \land [2 \in X \rightarrow 3\in Y]$. Is it possible, in first-order logic, to substitute the statements $2\in Y$ and $3\in Y$ by $1+1\in Y$ and $2+1\in Y$ respectively, thus, concluding that the entire expression is equivalent to $[1 \in X \rightarrow 1+1 \in Y] \land [2 \in X \rightarrow 2+1\in Y]$ and to the mapping $\forall x \in X \hspace{0.5em} \exists y \in Y \hspace{0.5em} y = x+1$?

Answer 1

Yes, using the substitution axiom for equality:

$x=y \to (\varphi \to \varphi')$, where $\varphi'$ is obtained from $\varphi$ replacing any number of free occurrences of $x$ with $y$.

Thus, provided that we have an axiom of theorem stating that $1+1=2$, we can use it with formula $\varphi := [1∈X → 2∈Y] ∧ [2∈X → 3∈Y]$ to get $[1∈X → 1+1∈Y]∧[1+1∈X → 3∈Y]$, and then replace $3$.