For cardinal arithmetic, we follow [Mendelson] p. 258. Rather than defining operations restricted to cardinal numbers, we use disjoint union df-dju () for cardinal addition, Cartesian product df-xp () for cardinal multiplication, and set exponentiation df-map () for cardinal exponentiation. Equinumerosity and dominance serve the roles of equality and ordering. If we wanted to, we could easily convert our theorems to actual cardinal number operations via carden, carddom, and cardsdom. The advantage of Mendelson's approach is that we can directly use many equinumerosity theorems that we already have available.