A model of ZF set theory language

Summary. The goal of this article is to construct a language of the ZF set theory and to develop a notational and conceptual base which facilitates a convenient usage of the language. MML Identifier:ZF_LANG. WWW:http://mizar.org/JFM/Vol1/zf_lang.html The articles [4], [6], [7], [3], [1], [5], and [2] provide the notation and terminology for this paper. For simplicity, we follow the rules: k, n are natural numbers, a is a set, D is a non empty set, and p, q are finite sequences of elements of N. The subset VAR of N is defined by: (Def. 1) VAR = {k: 5 ≤ k}. Let us observe that VAR is non empty. A variable is an element of VAR. Let us consider n. The functor xn yielding a variable is defined by: (Def. 2) xn = 5+n. In the sequel x, y, z, t denote variables