Metamath Proof Explorer


Table of Contents - 8.1.5. Isomorphic objects

In this subsection, the "is isomorphic to" relation between objects of a category is defined (see df-cic). It is shown that this relation is an equivalence relation, see cicer.

  1. ccic
  2. df-cic
  3. cicfval
  4. brcic
  5. cic
  6. brcici
  7. cicref
  8. ciclcl
  9. cicrcl
  10. cicsym
  11. cictr
  12. cicer