Metamath Proof Explorer

Definition df-frgr

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 thefriendship 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) (Revised by AV, 3-Jan-2024)

Ref Expression
Assertion df-frgr ⊢FriendGraph=g∈USGraph|[˙Vtx⁡g/v]˙[˙Edg⁡g/e]˙∀k∈v∀l∈v∖k∃!x∈vxkxl⊆e

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrgr classFriendGraph
1 vg setvarg
2 cusgr classUSGraph
3 cvtx classVtx
4 1 cv setvarg
5 4 3 cfv classVtx⁡g
6 vv setvarv
7 cedg classEdg
8 4 7 cfv classEdg⁡g
9 ve setvare
10 vk setvark
11 6 cv setvarv
12 vl setvarl
13 10 cv setvark
14 13 csn classk
15 11 14 cdif classv∖k
16 vx setvarx
17 16 cv setvarx
18 17 13 cpr classxk
19 12 cv setvarl
20 17 19 cpr classxl
21 18 20 cpr classxkxl
22 9 cv setvare
23 21 22 wss wffxkxl⊆e
24 23 16 11 wreu wff∃!x∈vxkxl⊆e
25 24 12 15 wral wff∀l∈v∖k∃!x∈vxkxl⊆e
26 25 10 11 wral wff∀k∈v∀l∈v∖k∃!x∈vxkxl⊆e
27 26 9 8 wsbc wff[˙Edg⁡g/e]˙∀k∈v∀l∈v∖k∃!x∈vxkxl⊆e
28 27 6 5 wsbc wff[˙Vtx⁡g/v]˙[˙Edg⁡g/e]˙∀k∈v∀l∈v∖k∃!x∈vxkxl⊆e
29 28 1 2 crab classg∈USGraph|[˙Vtx⁡g/v]˙[˙Edg⁡g/e]˙∀k∈v∀l∈v∖k∃!x∈vxkxl⊆e
30 0 29 wceq wffFriendGraph=g∈USGraph|[˙Vtx⁡g/v]˙[˙Edg⁡g/e]˙∀k∈v∀l∈v∖k∃!x∈vxkxl⊆e