cinv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cinv		Structured version Visualization version GIF version

Syntax Definition cinv 17457

Description: Extend class notation with the inverses of a morphism.

**Assertion**
Ref	Expression
cinv	class Inv

See definition df-inv 17460 for more information.

Colors of variables: wff setvar class