Yes, the axioms do trivially prove themselves. Your last derivation, however, is not valid: "A=A" can not be substituted for A because the latter is a symbol in a formal system, while the former is an object of it. You are free to postulate identity law as applied to symbols or laws, of course, in addition to just the identity law for objects, but that is a separate meta-law. I think OP's intuition might be of something like the universalist conception of logic that logicists envisioned, where everything has to be justified from within the system, and hence some axioms must be at the foundation and "unprovable". This, of course, is very different from the modern theory of formal systems, where (following Hilbert) meta-linguistic manipulations are "silently granted" without axiomatizing them in the system itself. If need be, a separate meta-language can be introduced for that purpose.
The confusion is understandable since, in Hilbertian terms, the universalist conception mixes the object language of the formal system with the meta-language used to talk about statements of that language, see semantic theory of truth. These were separated by Tarski exactly to avoid the paradoxes of self-reference, after Gödel's incompleteness results made the universalist logicism unattractive. Tarski proved that a formal first order theory that contains Peano arithmetic and is capable of expressing claims about the truth of its sentences, is necessarily inconsistent. This is his Undefinability of Truth theorem, and it might be the "one of the implications of Gödel" mentioned in the OP:
"This implies a major limitation on the scope of "self-representation." It is possible to define a formula True(n) whose extension is T but only by drawing on a metalanguage whose expressive power goes beyond that of L. For example, a truth predicate for first-order arithmetic can be defined in second-order arithmetic. However, this formula would only be able to define a truth predicate for sentences in the original language L. To define a truth predicate for the metalanguage would require a still higher "metametalanguage", and so on."
The requisite tower of meta-languages is known as the Tarski hierarchy. It is this hierarchy that prevents things like the Liar sentence "I am not true" from being formally expressible.
Now to another "implication of Gödel", Löb's theorem, which deriving A from A "can be shown to violate", according to the OP's earlier question. Of course, no such thing can be shown, but it does not help that Wikipedia's "formulation" of the Löb's theorem is highly misleading:
"in any formal system F with Peano arithmetic (PA), for any formula P, if it is provable in F that "if P is provable in F then P is true", then P is provable in F".
It can not be "provable in F" that "if P is provable in F then P is true", because such a thing would require F to contain its own truth predicate, and hence be inconsistent by the Undefinability of Truth. SEP gives a precise formulation of the Löb's theorem, and explains why Wikipedia's "lame terms" version of it is, well, lame:
"In order to understand Löb's theorem properly it is useful to first consider the so-called “reflection principles”. Above, the focus has been on expressing, inside a formal system, that the system is consistent, i.e., on Cons(F). But naturally the theory should not merely be consistent but also sound, i.e., prove only true sentences. How should the soundness of a system, i.e., the claim that everything derivable in the system is true, be expressed? If one wants to express this in the language of the system itself, it cannot be done by a single statement saying this, because there is, by the undefinability of truth, no suitable truth predicate available in the language. Various restricted and unrestricted soundness claims can, however, be expressed in the form of a scheme, the so-called Reflection Principles...
Exactly which instances of the reflection scheme are actually provable in the system? Löb's Theorem gives a precise answer to this question (assuming that Prov_F(x) satisfies the derivability conditions). [...] the instances of soundness (reflection principle) provable in a system are exactly the ones which concern sentences which are themselves provable in the system."