Definition df-frgr 27121

Description: Define the class of all friendship graphs: a simple graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. This condition is called the friendship condition , see definition in [MertziosUnger] p. 152. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017.) (Revised by AV, 29-Mar-2021.)

Assertion

Ref	Expression
df-frgr	|- FriendGraph = { g | ( g e. USGraph /\ [. (Vtx ` g ) / v ]. [. (Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e ) }

Distinct variable group:   e, g, k, l, x, v

Detailed syntax breakdown of Definition df-frgr

Step	Hyp	Ref	Expression
1		cfrgr 27120	. 2 class FriendGraph
2		vg	. . . . . 6 setvar g
3	2	cv 1482	. . . . 5 class g
4		cusgr 26044	. . . . 5 class USGraph
5	3, 4	wcel 1990	. . . 4 wff g e. USGraph
6		vx	. . . . . . . . . . . . 13 setvar x
7	6	cv 1482	. . . . . . . . . . . 12 class x
8		vk	. . . . . . . . . . . . 13 setvar k
9	8	cv 1482	. . . . . . . . . . . 12 class k
10	7, 9	cpr 4179	. . . . . . . . . . 11 class { x , k }
11		vl	. . . . . . . . . . . . 13 setvar l
12	11	cv 1482	. . . . . . . . . . . 12 class l
13	7, 12	cpr 4179	. . . . . . . . . . 11 class { x , l }
14	10, 13	cpr 4179	. . . . . . . . . 10 class { { x , k } , { x , l } }
15		ve	. . . . . . . . . . 11 setvar e
16	15	cv 1482	. . . . . . . . . 10 class e
17	14, 16	wss 3574	. . . . . . . . 9 wff { { x , k } , { x , l } } C_ e
18		vv	. . . . . . . . . 10 setvar v
19	18	cv 1482	. . . . . . . . 9 class v
20	17, 6, 19	wreu 2914	. . . . . . . 8 wff E! x e. v { { x , k } , { x , l } } C_ e
21	9	csn 4177	. . . . . . . . 9 class { k }
22	19, 21	cdif 3571	. . . . . . . 8 class ( v \ { k } )
23	20, 11, 22	wral 2912	. . . . . . 7 wff A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e
24	23, 8, 19	wral 2912	. . . . . 6 wff A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e
25		cedg 25939	. . . . . . 7 class Edg
26	3, 25	cfv 5888	. . . . . 6 class (Edg ` g )
27	24, 15, 26	wsbc 3435	. . . . 5 wff [. (Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e
28		cvtx 25874	. . . . . 6 class Vtx
29	3, 28	cfv 5888	. . . . 5 class (Vtx ` g )
30	27, 18, 29	wsbc 3435	. . . 4 wff [. (Vtx ` g ) / v ]. [. (Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e
31	5, 30	wa 384	. . 3 wff ( g e. USGraph /\ [. (Vtx ` g ) / v ]. [. (Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e )
32	31, 2	cab 2608	. 2 class { g | ( g e. USGraph /\ [. (Vtx ` g ) / v ]. [. (Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e ) }
33	1, 32	wceq 1483	1 wff FriendGraph = { g | ( g e. USGraph /\ [. (Vtx ` g ) / v ]. [. (Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e ) }

This definition is referenced by:  isfrgr  27122