This paper presents a formalization of axiomatic set theory, which is based on Morse-Kelley system but simplified adequately, and it can be used to formalize mathematical analysis. Firstly, we introduce comprehensively the Morse-Kelley axiomatic set theory (MK) including constants, definitions, axioms and so on. Moreover, we extracted the essential contents in MK to construct the mathematical analysis, where the recursive functions related to natural number operations is the foundation core. Therefore, the Recursion Theorem is proved by the Transfinite Recursion Theorem from MK, and further the definition of the recursive function can be obtained. At last, we use Landau’s Foundations of Analysis as roadmap to present how to implement mathematical analysis based on axiomatic set theory. All the constants, definitions, axioms, theorems had been formalized and proof details had been formally checked by Coq proof assistant, which can guarantee the readability and rigor. This work can be further applied to develop the more formalizations of Real Variable Function Theory, Topology, aerospace and other fields.