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 \in V ⟼ \{v \in Vtx (g) \| \forall n \in (Vtx (g) ∖ \{v\}) n \in (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 \in (g NeighbVtx v)$
15	14 7 10	wral	$wff \forall n \in (Vtx (g) ∖ \{v\}) n \in (g NeighbVtx v)$
16	15 3 6	crab	$class \{v \in Vtx (g) \| \forall n \in (Vtx (g) ∖ \{v\}) n \in (g NeighbVtx v)\}$
17	1 2 16	cmpt	$class (g \in V ⟼ \{v \in Vtx (g) \| \forall n \in (Vtx (g) ∖ \{v\}) n \in (g NeighbVtx v)\})$
18	0 17	wceq	$wff UnivVtx = (g \in V ⟼ \{v \in Vtx (g) \| \forall n \in (Vtx (g) ∖ \{v\}) n \in (g NeighbVtx v)\})$

Metamath Proof Explorer

Definition df-uvtx

Detailed syntax breakdown