What is a wellfounded relation, and how does wellfoundedness underpin wellfounded induction?

A formula $\phi(x, y)$ with two free variables defines an $\in$-automorphism if for all $x$ there is a unique $y$, the function $f$, defined by $y=f(x)$ if and only if $\phi(x, y)$, is a permutation of the universe, and we have $(\forall x y)(x \in y \leftrightarrow f(x) \in f(y))$.

Use wellfounded induction over $\in$ to prove that all formulæ defining $\in$-automorphisms are equivalent to $x=y$.