Table of ContentsTable of Contents User Sandbox < Previous   Next >
Related theorems
Unicode version
Syntax Definition ccod_ 10596
Description: Extend class notation with the function returning the function codomain of a category.
Assertion
Ref Expression
ccod_ class cod
See definition df-coda 10601 for more information.
Colors of variables: wff set class
Copyright terms: Public domain