MPE Home 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  =  ( v  e.  _V , 
e  e.  _V  |->  { n  e.  v  | 
A. k  e.  ( v  \  { n } ) { k ,  n }  e.  ran  e } )
Distinct variable group:    v, e, k, n

Detailed syntax breakdown of Definition df-uvtx
StepHypRef Expression
1 cuvtx 24397 . 2  class UnivVertex
2 vv . . 3  setvar  v
3 ve . . 3  setvar  e
4 cvv 3095 . . 3  class  _V
5 vk . . . . . . . 8  setvar  k
65cv 1382 . . . . . . 7  class  k
7 vn . . . . . . . 8  setvar  n
87cv 1382 . . . . . . 7  class  n
96, 8cpr 4016 . . . . . 6  class  { k ,  n }
103cv 1382 . . . . . . 7  class  e
1110crn 4990 . . . . . 6  class  ran  e
129, 11wcel 1804 . . . . 5  wff  { k ,  n }  e.  ran  e
132cv 1382 . . . . . 6  class  v
148csn 4014 . . . . . 6  class  { n }
1513, 14cdif 3458 . . . . 5  class  ( v 
\  { n }
)
1612, 5, 15wral 2793 . . . 4  wff  A. k  e.  ( v  \  {
n } ) { k ,  n }  e.  ran  e
1716, 7, 13crab 2797 . . 3  class  { n  e.  v  |  A. k  e.  ( v  \  { n } ) { k ,  n }  e.  ran  e }
182, 3, 4, 4, 17cmpt2 6283 . 2  class  ( v  e.  _V ,  e  e.  _V  |->  { n  e.  v  |  A. k  e.  ( v  \  { n } ) { k ,  n }  e.  ran  e } )
191, 18wceq 1383 1  wff UnivVertex  =  ( v  e.  _V , 
e  e.  _V  |->  { n  e.  v  | 
A. k  e.  ( v  \  { n } ) { k ,  n }  e.  ran  e } )
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