In his article "THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS", Paul Cohen writes in the beginning:
We shall work with the usual axioms for Zermelo-Fraenkel set theory, and by Z-F we shall denote these axioms without the Axiom of Choice, (but with the Axiom of Regularity).
Thus the meta-theory he is working in is the Zermelo-Fraenkel set theory without AC, but with the axiom of regularity. In this meta-theory, Cohen proves his famous result that CH is indepedent of ZFC. Now I wonder:
Did he use the regularity axiom of his meta-theory in his proof?