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	|- ComplGraph
1		vg	|- g
2		cuvtx	|- UnivVtx
3	1	cv	|- g
4	3 2	cfv	|- ( UnivVtx ` g )
5		cvtx	|- Vtx
6	3 5	cfv	|- ( Vtx ` g )
7	4 6	wceq	|- ( UnivVtx ` g ) = ( Vtx ` g )
8	7 1	cab	|- { g | ( UnivVtx ` g ) = ( Vtx ` g ) }
9	0 8	wceq	|- ComplGraph = { g | ( UnivVtx ` g ) = ( Vtx ` g ) }