Bounded Zermelo set theory, and many variants named for MacLane in some way, are used in equiconsistency proofs for Simple Theory of Types plus infinity, and for the Elementary Theory of the Category of Sets starting in 1969 (see Finite order arithmetic and ETCS). But did anyone formulate it before that?
Of course Bounded Zermelo could easily have been stated before that, and the analogy with Primitive Recursive Arithmetic could have suggested it. But was it formulated earlier in fact?