Note that Halmos is not working in a formal context. However, sometimes authors who work even in a formal context do include such existence axioms. Some of those authors mention that they do that only for purposes of convenience since we really don't need such an axiom. Other authors who adopt such an axiom don't even bother discussing it much. But in any case, whether included as a formal axiom or not, it is superfluous, as is the empty set axiom, when we have the axiom schema of separation either as a theorem schema from the axiom schema of replacement or as its own independent axiom schema.
Halmos does this in Naive Set Theory, making an official assumption that "there exists a set".