cretr - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cretr		Structured version Visualization version Unicode version

Syntax Definition cretr 31199

Description: Extend class notation with the retract relation.

**Assertion**
Ref	Expression
cretr	Retr

See definition df-retr 31200 for more information.

Colors of variables: wff setvar class