Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-uvtx Structured version   Unicode version

Definition df-uvtx 24400
 Description: Define the class of all universal vertices (in graphs). A vertex is called universal if it is adjacent, i.e. connected by an edge, to all other vertices (of the graph). (Contributed by Alexander van der Vekens, 12-Oct-2017.)
Assertion
Ref Expression
df-uvtx UnivVertex
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-uvtx
StepHypRef Expression
1 cuvtx 24397 . 2 UnivVertex
2 vv . . 3
3 ve . . 3
4 cvv 3095 . . 3
5 vk . . . . . . . 8
65cv 1382 . . . . . . 7
7 vn . . . . . . . 8
87cv 1382 . . . . . . 7
96, 8cpr 4016 . . . . . 6
103cv 1382 . . . . . . 7
1110crn 4990 . . . . . 6
129, 11wcel 1804 . . . . 5
132cv 1382 . . . . . 6
148csn 4014 . . . . . 6
1513, 14cdif 3458 . . . . 5
1612, 5, 15wral 2793 . . . 4
1716, 7, 13crab 2797 . . 3
182, 3, 4, 4, 17cmpt2 6283 . 2
191, 18wceq 1383 1 UnivVertex
 Colors of variables: wff setvar class This definition is referenced by:  isuvtx  24466  uvtxisvtx  24468  uvtx0  24469  uvtx01vtx  24470
 Copyright terms: Public domain W3C validator