Ah, Thomas Forster's 1998 paper "Weak systems of set theory related to HOL"
- Forster T. (1994) Weak systems of set theory related to HOL. In: Melham T.F., Camilleri J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. doi:10.1007/3-540-58450-1_43
is available on-line at various places including https://www.dpmms.cam.ac.uk/~tf/maltapaper.pshere.
He says it is proved in
Jensen RB "On the consistency of a slight (?) modification of Quine's NF" Synthese 19 1969 pp 25--63.
Lake J "Comparing Type theory and Set theory" Zeitschrift fur Matematische Logik 21 1975 pp 355-56.
Jensen RB, On the consistency of a slight (?) modification of Quine's NF, Synthese 19 1969 pp 25--63, doi:10.1007/978-94-010-1709-1_16
Lake J, Comparing Type theory and Set theory, Zeitschrift fur Matematische Logik 21 1975 pp 355-56. doi:10.1002/malq.19750210144
For a fanatically detailed proof and discussion see Mathias at https://www.dpmms.cam.ac.uk/~ardm/maclane.pdf
- Mathias, A. R. D. The strength of Mac Lane set theory. Ann. Pure Appl. Logic 110 (2001), no. 1-3, 107–234, doi:10.1016/S0168-0072(00)00031-2, author pdf
