Definition df-cusgr 27779

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 27821. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.) (Revised by BJ, 14-Feb-2022.)

Assertion

Ref	Expression
df-cusgr	⊢ ComplUSGraph = (USGraph ∩ ComplGraph)

Detailed syntax breakdown of Definition df-cusgr

Step	Hyp	Ref	Expression
1		ccusgr 27777	. 2 class ComplUSGraph
2		cusgr 27519	. . 3 class USGraph
3		ccplgr 27776	. . 3 class ComplGraph
4	2, 3	cin 3886	. 2 class (USGraph ∩ ComplGraph)
5	1, 4	wceq 1539	1 wff ComplUSGraph = (USGraph ∩ ComplGraph)

This definition is referenced by:  iscusgr  27785