Here we extend the language of wffs with predicate calculus, which allows us to talk about individual objects in a domain of discourse (which for us will be the universe of all sets, so we call them "setvar variables") and make true/false statements about predicates, which are relationships between objects, such as whether or not two objects are equal. In addition, we introduce universal quantification ("for all", e.g. ax-4) in order to make statements about whether a wff holds for every object in the domain of discourse. Later we introduce existential quantification ("there exists", df-ex) which is defined in terms of universal quantification.
Our axioms are really axiom schemes, and our wff and setvar variables are metavariables ranging over expressions in an underlying "object language". This is explained here: mmset.html#axiomnote.
Our axiom system starts with the predicate calculus axiom schemes system S2 of Tarski defined in his 1965 paper, "A Simplified Formalization of Predicate Logic with Identity" [Tarski]. System S2 is defined in the last paragraph on p. 77, and repeated on p. 81 of [KalishMontague]. We do not include scheme B5 (our sp) of system S2 since [KalishMontague] shows it to be logically redundant (Lemma 9, p. 87, which we prove as theorem spw below).
Theorem spw can be used to prove any instance of sp having mutually distinct setvar variables and no wff metavariables. However, it seems that sp in its general form cannot be derived from only Tarski's schemes. We do not include B5 i.e. sp as part of what we call "Tarski's system" because we want it to be the smallest set of axioms that is logically complete with no redundancies. We later prove sp as theorem axc5 using the auxiliary axiom schemes that make our system metalogically complete.
Our version of Tarski's system S2 consists of propositional calculus (ax-mp, ax-1, ax-2, ax-3) plus ax-gen, ax-4, ax-5, ax-6, ax-7, ax-8, and ax-9. The last three are equality axioms that represent three sub-schemes of Tarski's scheme B8. Due to its side-condition ("where is an atomic formula and is obtained by replacing an occurrence of the variable by the variable "), we cannot represent his B8 directly without greatly complicating our scheme language, but the simpler schemes ax-7, ax-8, and ax-9 are sufficient for set theory and much easier to work with.
Tarski's system is exactly equivalent to the traditional axiom system in most logic textbooks but has the advantage of being easy to manipulate with a computer program, and its simpler metalogic (with no built-in notions of "free variable" and "proper substitution") is arguably easier for a non-logician human to follow step by step in a proof (where "follow" means being able to identify the substitutions that were made, without necessarily a higher-level understanding). In particular, it is logically complete in that it can derive all possible object-language theorems of predicate calculus with equality, i.e., the same theorems as the traditional system can derive.
However, for efficiency (and indeed a key feature that makes Metamath successful), our system is designed to derive reusable theorem schemes (rather than object-language theorems) from other schemes. From this "metalogical" point of view, Tarski's S2 is not complete. For example, we cannot derive scheme sp, even though (using spw) we can derive all instances of it that do not involve wff metavariables or bundled setvar variables. (Two setvar variables are "bundled" if they can be substituted with the same setvar variable, i.e., do not have a "$d" disjoint variable condition.) Later we will introduce auxiliary axiom schemes ax-10, ax-11, ax-12, and ax-13 that are metatheorems of Tarski's system (i.e. are logically redundant) but which give our system the property of "scheme completeness", allowing us to prove directly (instead of, say, by induction on formula length) all possible schemes that can be expressed in our language.