Metamath Proof Explorer


Definition df-cplgr

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)

Ref Expression
Assertion df-cplgr ComplGraph = g | UnivVtx g = Vtx g

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccplgr class ComplGraph
1 vg setvar g
2 cuvtx class UnivVtx
3 1 cv setvar g
4 3 2 cfv class UnivVtx g
5 cvtx class Vtx
6 3 5 cfv class Vtx g
7 4 6 wceq wff UnivVtx g = Vtx g
8 7 1 cab class g | UnivVtx g = Vtx g
9 0 8 wceq wff ComplGraph = g | UnivVtx g = Vtx g