Definition df-cplgr 26231

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. (Contributed by AV, 24-Oct-2020.)

Assertion

Ref	Expression
df-cplgr	|- ComplGraph = { g | A. v e. (Vtx ` g ) v e. (UnivVtx ` g ) }

Distinct variable group:   v, g

Detailed syntax breakdown of Definition df-cplgr

Step	Hyp	Ref	Expression
1		ccplgr 26226	. 2 class ComplGraph
2		vv	. . . . . 6 setvar v
3	2	cv 1482	. . . . 5 class v
4		vg	. . . . . . 7 setvar g
5	4	cv 1482	. . . . . 6 class g
6		cuvtxa 26225	. . . . . 6 class UnivVtx
7	5, 6	cfv 5888	. . . . 5 class (UnivVtx ` g )
8	3, 7	wcel 1990	. . . 4 wff v e. (UnivVtx ` g )
9		cvtx 25874	. . . . 5 class Vtx
10	5, 9	cfv 5888	. . . 4 class (Vtx ` g )
11	8, 2, 10	wral 2912	. . 3 wff A. v e. (Vtx ` g ) v e. (UnivVtx ` g )
12	11, 4	cab 2608	. 2 class { g | A. v e. (Vtx ` g ) v e. (UnivVtx ` g ) }
13	1, 12	wceq 1483	1 wff ComplGraph = { g | A. v e. (Vtx ` g ) v e. (UnivVtx ` g ) }

This definition is referenced by:  iscplgr  26310