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

Definition df-cusgr 26153
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 26271. (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
StepHypRef Expression
1 ccusgr 26148 . 2 class ComplUSGraph
2 vg . . . . 5 setvar 𝑔
32cv 1479 . . . 4 class 𝑔
4 ccplgr 26147 . . . 4 class ComplGraph
53, 4wcel 1987 . . 3 wff 𝑔 ∈ ComplGraph
6 cusgr 25971 . . 3 class USGraph
75, 2, 6crab 2912 . 2 class {𝑔 ∈ USGraph ∣ 𝑔 ∈ ComplGraph}
81, 7wceq 1480 1 wff ComplUSGraph = {𝑔 ∈ USGraph ∣ 𝑔 ∈ ComplGraph}
Colors of variables: wff setvar class
This definition is referenced by:  iscusgr  26235
  Copyright terms: Public domain W3C validator