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

Definition df-frgra 30552
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 30551 . 2  class FriendGrph
2 vv . . . . . 6  setvar  v
32cv 1368 . . . . 5  class  v
4 ve . . . . . 6  setvar  e
54cv 1368 . . . . 5  class  e
6 cusg 23232 . . . . 5  class USGrph
73, 5, 6wbr 4287 . . . 4  wff  v USGrph  e
8 vx . . . . . . . . . . 11  setvar  x
98cv 1368 . . . . . . . . . 10  class  x
10 vk . . . . . . . . . . 11  setvar  k
1110cv 1368 . . . . . . . . . 10  class  k
129, 11cpr 3874 . . . . . . . . 9  class  { x ,  k }
13 vl . . . . . . . . . . 11  setvar  l
1413cv 1368 . . . . . . . . . 10  class  l
159, 14cpr 3874 . . . . . . . . 9  class  { x ,  l }
1612, 15cpr 3874 . . . . . . . 8  class  { {
x ,  k } ,  { x ,  l } }
175crn 4836 . . . . . . . 8  class  ran  e
1816, 17wss 3323 . . . . . . 7  wff  { {
x ,  k } ,  { x ,  l } }  C_  ran  e
1918, 8, 3wreu 2712 . . . . . 6  wff  E! x  e.  v  { { x ,  k } ,  { x ,  l } }  C_  ran  e
2011csn 3872 . . . . . . 7  class  { k }
213, 20cdif 3320 . . . . . 6  class  ( v 
\  { k } )
2219, 13, 21wral 2710 . . . . 5  wff  A. l  e.  ( v  \  {
k } ) E! x  e.  v  { { x ,  k } ,  { x ,  l } }  C_ 
ran  e
2322, 10, 3wral 2710 . . . 4  wff  A. k  e.  v  A. l  e.  ( v  \  {
k } ) E! x  e.  v  { { x ,  k } ,  { x ,  l } }  C_ 
ran  e
247, 23wa 369 . . 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 4344 . 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 1369 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 setvar class
This definition is referenced by:  isfrgra  30553  frisusgrapr  30554
  Copyright terms: Public domain W3C validator