Some people do have to care about such details, at least in unusual contexts, and I do think it’s generally worth being aware of your foundations. The details of the definition of ordered pairs is crucial in Quine’s New Foundations (e.g., http://en.wikipedia.org/wiki/New_Foundations#Ordered_pairs), and taking it as primitive can have actual set-theoretic consequences in NF. In Church’s unpublished supplement to his “Set Theory with a Universal Set,” he uses a deliberately ugly [my interpretation] definition of m-tuple to avoid collisions. In my follow-on work, I use the usual Kuratowski definition of ordered pairs, since their internal structure allowed me to model the singleton function as a set, since it’s a 2-equivalence class, for a generalization of Church’s definition of j-equivalence relations.

Some people do have to care about such details, at least in unusual contexts, and I do think it’s generally worth being aware of your foundations. The details of the definition of ordered pairs is crucial in Quine’s New Foundations (e.g., https://en.wikipedia.org/wiki/New_Foundations#Ordered_pairs), and taking it as primitive can have actual set-theoretic consequences in NF. In Church’s unpublished supplement to his “Set Theory with a Universal Set,” he uses a deliberately ugly [my interpretation] definition of m-tuple to avoid collisions. In my follow-on work, I use the usual Kuratowski definition of ordered pairs, since their internal structure allowed me to model the singleton function as a set, since it’s a 2-equivalence class, for a generalization of Church’s definition of j-equivalence relations.