ccom - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer	< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ccom		Structured version GIF version

Syntax Definition ccom 4292

Description: Extend the definition of a class to include the composition of two classes. (Read: The composition of A and B.)

**Hypotheses**
Ref	Expression
cA	class A
cB	class B

**Assertion**
Ref	Expression
ccom	class (A ∘ B)

See definition df-co 4297 for more information.

Colors of variables: wff set class