Definition. bij_equi
bij f X Y ↔ inj f X Y ∧ sur f X Y