Definition df-cusgr 40558

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

Assertion

Ref	Expression
df-cusgr	⊢ ComplUSGraph = {𝑔 ∈ USGraph ∣ 𝑔 ∈ ComplGraph}

Detailed syntax breakdown of Definition df-cusgr

Step	Hyp	Ref	Expression
1		ccusgr 40553	. 2 class ComplUSGraph
2		vg	. . . . 5 setvar 𝑔
3	2	cv 1474	. . . 4 class 𝑔
4		ccplgr 40552	. . . 4 class ComplGraph
5	3, 4	wcel 1977	. . 3 wff 𝑔 ∈ ComplGraph
6		cusgr 40379	. . 3 class USGraph
7	5, 2, 6	crab 2900	. 2 class {𝑔 ∈ USGraph ∣ 𝑔 ∈ ComplGraph}
8	1, 7	wceq 1475	1 wff ComplUSGraph = {𝑔 ∈ USGraph ∣ 𝑔 ∈ ComplGraph}

This definition is referenced by:  iscusgr  40640