cedga - Metamath Proof Explorer

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

Syntax Definition cedga 25792

Description: Extend class notation with the set of edges (of an undirected simple (pseudo)graph) Remark: TODO-AV: If this definition (and all related theorems) are moved to main.set, the label should become "cedg".

**Assertion**
Ref	Expression
cedga	class Edg

See definition df-edga 25793 for more information.

Colors of variables: wff setvar class

W3C validator