Description: Membership in a class abstraction of ordered pairs. Weaker version of elopab with a sethood antecedent, avoiding ax-sep , ax-nul , and ax-pr . Originally a subproof of elopab . (Contributed by SN, 11-Dec-2024)