Well, stepping back from a specific axiomatization of set theory for a second, there are 3 ways to define a set (or class) (haha, I've said this exact thing before here, so I'll just copy+paste):
1) Extension -- name all members of S.
2) Intension -- name a definite property that all members of S have.
a) basis clause -- name at least one member of S.
b) induction clause -- give rule(s) to get more members from those in (a) -- if x is in S, then x' is in S.
c) extremal clause -- says that nothing else is in S.
If the set is finite, you can simply list its members.
I imagine you don't need very liberal axioms to allow that. Maybe it would be a useful exercise to look at each axiom and identify which method it uses. For example, the Axiom of Pairing uses (1).
Oh, I should probably try to head off any confusion or complaints by noting that a proof is usually defined to be finite in length.
Also, (1) will only give you a finite set, if that wasn't clear. (If you can furthermore only invoke a (1)-type axiom a finite number of times, as is the case for finite-length proofs, can you ever prove the existence of any infinite set that way (assuming you didn't already have one)?)