Just had a look at a transcript of Gödel's 1931, On formally undecidable propositions of Principia Mathematica here. The original is found for example here. There is a particular axiom schema V on page numbered 178.
I noticed that his system, which he formalizes, uses very few axioms schemas and inference rules. Its basically a higher-order calculus with typed variables. One of the axiom schemas, not showing the typing of the variables, is as follows:
Axiom Schema V: $$\forall z(x(z) \leftrightarrow y(z)) \rightarrow x = y$$
I wonder why Gödel didn't put a bi-implication in the above and only an implication. So my question is can we somehow derive strictly in his explicitly mentioned axiom schemas and inference rules the converse:
$$x = y \rightarrow \forall z(x(z) \leftrightarrow y(z)) \quad ?$$
Or alternatively how in Gödels system could be shown the simpler form a substitution property, which would also imply the converse:
$$x = y \wedge x(z) \rightarrow y(z) \quad ?$$
Anybody knowledgeable in this matter? Note that this answer here is not a duplicate, since the answer assumes the substitution property, but we would need to first show that Gödels system admits the substitution property.