Definition df-cplgr 40557

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 = {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)𝑣 ∈ (UnivVtx‘𝑔)}

Distinct variable group:   𝑣,𝑔

Detailed syntax breakdown of Definition df-cplgr

Step	Hyp	Ref	Expression
1		ccplgr 40552	. 2 class ComplGraph
2		vv	. . . . . 6 setvar 𝑣
3	2	cv 1474	. . . . 5 class 𝑣
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1474	. . . . . 6 class 𝑔
6		cuvtxa 40551	. . . . . 6 class UnivVtx
7	5, 6	cfv 5804	. . . . 5 class (UnivVtx‘𝑔)
8	3, 7	wcel 1977	. . . 4 wff 𝑣 ∈ (UnivVtx‘𝑔)
9		cvtx 25673	. . . . 5 class Vtx
10	5, 9	cfv 5804	. . . 4 class (Vtx‘𝑔)
11	8, 2, 10	wral 2896	. . 3 wff ∀𝑣 ∈ (Vtx‘𝑔)𝑣 ∈ (UnivVtx‘𝑔)
12	11, 4	cab 2596	. 2 class {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)𝑣 ∈ (UnivVtx‘𝑔)}
13	1, 12	wceq 1475	1 wff ComplGraph = {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)𝑣 ∈ (UnivVtx‘𝑔)}

This definition is referenced by:  iscplgr  40636