Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-frgra Unicode version

Definition df-frgra 28093
Description: Define the class of all Friendship Graphs. A graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017.)
Assertion
Ref Expression
df-frgra  |- FriendGrph  =  { <. v ,  e >.  |  ( v USGrph  e  /\  A. k  e.  v 
A. l  e.  ( v  \  { k } ) E! x  e.  v  { { x ,  k } ,  { x ,  l } }  C_  ran  e ) }
Distinct variable group:    v, e, k, l, x

Detailed syntax breakdown of Definition df-frgra
StepHypRef Expression
1 cfrgra 28092 . 2  class FriendGrph
2 vv . . . . . 6  set  v
32cv 1648 . . . . 5  class  v
4 ve . . . . . 6  set  e
54cv 1648 . . . . 5  class  e
6 cusg 21318 . . . . 5  class USGrph
73, 5, 6wbr 4172 . . . 4  wff  v USGrph  e
8 vx . . . . . . . . . . 11  set  x
98cv 1648 . . . . . . . . . 10  class  x
10 vk . . . . . . . . . . 11  set  k
1110cv 1648 . . . . . . . . . 10  class  k
129, 11cpr 3775 . . . . . . . . 9  class  { x ,  k }
13 vl . . . . . . . . . . 11  set  l
1413cv 1648 . . . . . . . . . 10  class  l
159, 14cpr 3775 . . . . . . . . 9  class  { x ,  l }
1612, 15cpr 3775 . . . . . . . 8  class  { {
x ,  k } ,  { x ,  l } }
175crn 4838 . . . . . . . 8  class  ran  e
1816, 17wss 3280 . . . . . . 7  wff  { {
x ,  k } ,  { x ,  l } }  C_  ran  e
1918, 8, 3wreu 2668 . . . . . 6  wff  E! x  e.  v  { { x ,  k } ,  { x ,  l } }  C_  ran  e
2011csn 3774 . . . . . . 7  class  { k }
213, 20cdif 3277 . . . . . 6  class  ( v 
\  { k } )
2219, 13, 21wral 2666 . . . . 5  wff  A. l  e.  ( v  \  {
k } ) E! x  e.  v  { { x ,  k } ,  { x ,  l } }  C_ 
ran  e
2322, 10, 3wral 2666 . . . 4  wff  A. k  e.  v  A. l  e.  ( v  \  {
k } ) E! x  e.  v  { { x ,  k } ,  { x ,  l } }  C_ 
ran  e
247, 23wa 359 . . 3  wff  ( v USGrph 
e  /\  A. k  e.  v  A. l  e.  ( v  \  {
k } ) E! x  e.  v  { { x ,  k } ,  { x ,  l } }  C_ 
ran  e )
2524, 2, 4copab 4225 . 2  class  { <. v ,  e >.  |  ( v USGrph  e  /\  A. k  e.  v  A. l  e.  ( v  \  { k } ) E! x  e.  v  { { x ,  k } ,  {
x ,  l } }  C_  ran  e ) }
261, 25wceq 1649 1  wff FriendGrph  =  { <. v ,  e >.  |  ( v USGrph  e  /\  A. k  e.  v 
A. l  e.  ( v  \  { k } ) E! x  e.  v  { { x ,  k } ,  { x ,  l } }  C_  ran  e ) }
Colors of variables: wff set class
This definition is referenced by:  isfrgra  28094  frisusgrapr  28095
  Copyright terms: Public domain W3C validator