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 e. _V |-> { v e. ( Vtx ` g ) | A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuvtx	|- UnivVtx
1		vg	|- g
2		cvv	|- _V
3		vv	|- v
4		cvtx	|- Vtx
5	1	cv	|- g
6	5 4	cfv	|- ( Vtx ` g )
7		vn	|- n
8	3	cv	|- v
9	8	csn	|- { v }
10	6 9	cdif	|- ( ( Vtx ` g ) \ { v } )
11	7	cv	|- n
12		cnbgr	|- NeighbVtx
13	5 8 12	co	|- ( g NeighbVtx v )
14	11 13	wcel	|- n e. ( g NeighbVtx v )
15	14 7 10	wral	|- A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v )
16	15 3 6	crab	|- { v e. ( Vtx ` g ) | A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v ) }
17	1 2 16	cmpt	|- ( g e. _V |-> { v e. ( Vtx ` g ) | A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v ) } )
18	0 17	wceq	|- UnivVtx = ( g e. _V |-> { v e. ( Vtx ` g ) | A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v ) } )