Definition df-cplgr 28665

Description: Define the class of all complete "graphs". A class/graph is called complete if every pair of distinct vertices is connected by an edge, i.e., each vertex has all other vertices as neighbors or, in other words, each vertex is a universal vertex. (Contributed by AV, 24-Oct-2020.) (Revised by TA, 15-Feb-2022.)

Assertion

Ref	Expression
df-cplgr	⊢ ComplGraph = {𝑔 ∣ (UnivVtx‘𝑔) = (Vtx‘𝑔)}

Detailed syntax breakdown of Definition df-cplgr

Step	Hyp	Ref	Expression
1		ccplgr 28663	. 2 class ComplGraph
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1540	. . . . 5 class 𝑔
4		cuvtx 28639	. . . . 5 class UnivVtx
5	3, 4	cfv 6543	. . . 4 class (UnivVtx‘𝑔)
6		cvtx 28253	. . . . 5 class Vtx
7	3, 6	cfv 6543	. . . 4 class (Vtx‘𝑔)
8	5, 7	wceq 1541	. . 3 wff (UnivVtx‘𝑔) = (Vtx‘𝑔)
9	8, 2	cab 2709	. 2 class {𝑔 ∣ (UnivVtx‘𝑔) = (Vtx‘𝑔)}
10	1, 9	wceq 1541	1 wff ComplGraph = {𝑔 ∣ (UnivVtx‘𝑔) = (Vtx‘𝑔)}

This definition is referenced by:  cplgruvtxb  28667