Although your argument doesn't prove the full Kunen inconsistency,
for the reasons already explained by Ali Enayat, it does prove the following form of the Kunen inconsistency, ruling out *definable* nontrivial elementary embeddings. What is more, it is often only this form of the result that one finds expressed by set theorists. For example, the version of the Kunen inconsistency stated in Kanamori's text is only this weaker form (see footnote 1 in the paper linked below).

**Theorem.** There is no definable class $j$ that is a nontrivial elementary embedding $j:V\to V$.

Proof: This is a theorem scheme of ZFC, with one theorem for each possible defining formula of $j$. Suppose first that $j:V\to V$ is a nontrivial elementary embedding and that $j(x)=y$ is defined by a formula
$\psi(x,y)$. We may then define the critical point of $j$, just as in your argument, and deduce by elementarity that $j(\kappa)$ would also have to be
the critical point, which is a contradiction. Thus, there is no
*definable* nontrivial elementary embedding $j:V\to V$.

One can adapt the argument to show that there is no nontrivial
elementary embedding $j:V\to V$ that is definable from parameters.
To do this, if $j(x)=y$ is defined by $\psi(x,y,z)$, with
parameter $z$, then you may assume $z$ is chosen so that this
embedding gives rise to the smallest possible critical point among
any parameter for which the definition does define an elementary
embedding (and this is itself definable, by asserting that the relation is $\Sigma_1$-elementary and cofinal). This defines $\kappa$
without parameters, and so again one attains a contradiction. QED

In particular, when one chooses to formalize the Kunen inconsistency as a result in ZFC, as opposed to the second order theories GBC or KM, then it admits of this very soft proof. Furthermore, this argument does not use the axiom of choice, and so actually it is provable in ZF. This argument was published by Suzuki in 1998. You will also find an
account of it and further generalizations in my paper
Generalizations of the Kunen Inconsistency, joint with Norman Perlmutter and Greg Kirmayer.

Our view, which we explain in the paper, is that this ZFC formulation of the Kunen inconsistency does not capture the full power of his argument. Kunen himself proved his theorem in Kelly-Morse KM set theory, although his argument and the other combinatorial proofs can be given in Gödel-Bernays GBC set theory, which gives a stronger result. Our paper contains several further generalizations of this argument, to treat nontrivial embeddings $j:V[G]\to V$ or $j:V\to V[G]$ that might be definable in a forcing extension $V[G]$ and many other cases.

ZFCsets. $\endgroup$ – theHigherGeometer Feb 27 '13 at 4:44