Metamath Proof Explorer

Definition df-uvtx

Description: Define the class of all universal vertices (in graphs). A vertex is calleduniversal if it is adjacent, i.e. connected by an edge, to all other vertices (of the graph), or equivalently, if all other vertices are its neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 24-Oct-2020)

Ref Expression
Assertion df-uvtx ⊢ UnivVtx = g ∈ V ⟼ v ∈ Vtx ⁡ g | ∀ n ∈ Vtx ⁡ g ∖ v n ∈ g NeighbVtx v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuvtx class UnivVtx
1 vg setvar g
2 cvv class V
3 vv setvar v
4 cvtx class Vtx
5 1 cv setvar g
6 5 4 cfv class Vtx ⁡ g
7 vn setvar n
8 3 cv setvar v
9 8 csn class v
10 6 9 cdif class Vtx ⁡ g ∖ v
11 7 cv setvar n
12 cnbgr class NeighbVtx
13 5 8 12 co class g NeighbVtx v
14 11 13 wcel wff n ∈ g NeighbVtx v
15 14 7 10 wral wff ∀ n ∈ Vtx ⁡ g ∖ v n ∈ g NeighbVtx v
16 15 3 6 crab class v ∈ Vtx ⁡ g | ∀ n ∈ Vtx ⁡ g ∖ v n ∈ g NeighbVtx v
17 1 2 16 cmpt class g ∈ V ⟼ v ∈ Vtx ⁡ g | ∀ n ∈ Vtx ⁡ g ∖ v n ∈ g NeighbVtx v
18 0 17 wceq wff UnivVtx = g ∈ V ⟼ v ∈ Vtx ⁡ g | ∀ n ∈ Vtx ⁡ g ∖ v n ∈ g NeighbVtx v