Where is axiom of regularity actually used? Why is it important? Are there some proofs, which are substantially simpler thanks to this axiom?
I have to admit that I do not know other use of this axiom than the proof that every set has rank in cumulative hierarchy, and a few easy consequences of this axiom, which are mentioned in Wikipedia article.
I remember seeing an introductory book in axiomatic set theory, which did not even mention this axiom. (And that book went through plenty of stuff, such as introducing ordinals, transfinite induction, construction of natural numbers.)
Based on the above, it seems that quite a lot of stuff can be done without this axiom.
Of course, it's quite possible that this axiom becomes important in some areas of set theory which are not familiar to me, such as forcing or working without Axiom of Choice. (It might be difficult to define cardinality without AC and regularity, as mentioned here.) But even if the this axiom is important only for some advanced stuff - which I will probably never get to - I'd be glad to know that.