Could you clarify what is $p$, please?

I was going to say that maybe "completeness theorems" or "embedding theorems" (for statements in 2-category theory) might be useful buzzphrases. But now I don't know whether you'll see this comment -- you deleted too quickly for me to insert this comment in time.

It seems that Borceux is probably basing himself on Linton, F.E.J. (1966). Some Aspects of Equational Categories. In: Eilenberg, S., Harrison, D.K., MacLane, S., Röhrl, H. (eds) Proceedings of the Conference on Categorical Algebra. Springer, Berlin, Heidelberg. doi.org/10.1007/978-3-642-99902-4_3, but with a slight difference in formulation. I'll try to track down what is going on here (although you might beat me to it).

Like varkor, I'm also feeling internal resistance to how you're using "internal language", and maybe even more resistance to "interpretation of the language of ZF". which is single-sorted with a single binary predicate $\in$. But it sounds like maybe you want embedding/completeness theorems in the 2-categorical context. So for example, in the 1-categorical context, to prove a general statement about finite limits, it suffices to prove it for Set, since we have the Yoneda embedding which is fully faithful and left exact, to do the remaining work.

Comments have been moved to chat; please do not continue the discussion here. Before posting a comment below this one, please review the purposes of comments. Comments that do not request clarification or suggest improvements usually belong as an answer, on MathOverflow Meta, or in MathOverflow Chat. Comments continuing discussion may be removed.

@PietroMajer Thanks for this! You never know when this stuff will come in handy. Jim Stasheff (golem.ph.utexas.edu/category/2009/11/…) told a story once: "but the worst was: i had picked up the math expression `to bugger a construction’ while at Princeton and used it in a lecture in Oxford with JHCW in the audience. He felt compelled to explain to me in Latin! the British meaning" (I guess you know, that's J.H.C. Whitehead).

Dear Professor Saitoh (or anyone else who has looked into the subject matter): could you please be more specific, either by quoting the precise result, or by pointing to a paragraph that gives examples of what the OP is after?

I'm very curious as to why someone downvoted this.

Comments have been moved to chat; please do not continue the discussion here. Before posting a comment below this one, please review the purposes of comments. Comments that do not request clarification or suggest improvements usually belong as an answer, on MathOverflow Meta, or in MathOverflow Chat. Comments continuing discussion may be removed.

My position is to keep that chat in place for the historical record. Moving forward, please keep in mind the norms that have developed over the history of this site, which before 2013 was not part of the SE network. If you ask a question and then decide to answer with something you had in mind all along, hitting the CW button would probably go a good distance in maintaining good will with the community, especially if you recognize and support other answers that contain insights you hadn't considered.

Comments have been moved to chat; please do not continue the discussion here. Before posting a comment below this one, please review the purposes of comments. Comments that do not request clarification or suggest improvements usually belong as an answer, on MathOverflow Meta, or in MathOverflow Chat. Comments continuing discussion may be removed.

As someone with a liking for symmetric function theory, you've managed to make me want to look (again) at the traditional proof!

@NoahSchweber Thank you so much for the information!

@Kapil Coming back to this after 8 years, I would tell my past self to discard this absurdly contorted argument (and I may do just that: delete the post, or completely rewrite it). Asaf was right. Just enumerate the elements $a_1, a_2, \ldots$, and build a maximal ideal $P$ by taking the union of ideals $P_n$ where $P_0 = \{0\}$, defining $P_n = P_{n-1} + \langle a_n\rangle$ if this is proper, else defining $P_n = P_{n-1}$.