Description: If two sets have equal nonzero cardinalities, then they are equinumerous. This assertion and carden2b are meant to replace carden in ZF without AC. (Contributed by Mario Carneiro, 9-Jan-2013)