Metamath Proof Explorer

Definition df-cusgr

Description: Define the class of all complete simple graphs. A simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge, see definition in section 1.1 of Diestel p. 3. In contrast, the definition in section I.1 of Bollobas p. 3 is based on the size of (finite) complete graphs, see cusgrsize . (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 24-Oct-2020) (Revised by BJ, 14-Feb-2022)

Ref Expression
Assertion df-cusgr ComplUSGraph = USGraph ComplGraph

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccusgr class ComplUSGraph
1 cusgr class USGraph
2 ccplgr class ComplGraph
3 1 2 cin class USGraph ComplGraph
4 0 3 wceq wff ComplUSGraph = USGraph ComplGraph