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.
Does this work? Use footnote 21 of Gödel's paper (which defines $x = y$ as $\forall W(Wx \equiv Wy)$.
And then use the type raising and lowering powers of Gödel's Axiom IV (to trade between x(z) and an equivalent Z(x)).