Definition df-uhgra 25821

Description: Define the class of all undirected hypergraphs. An undirected hypergraph is a pair of a set and a function into the powerset of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.)

Assertion

Ref	Expression
df-uhgra	⊢ UHGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})}

Distinct variable group:   𝑣,𝑒

Detailed syntax breakdown of Definition df-uhgra

Step	Hyp	Ref	Expression
1		cuhg 25819	. 2 class UHGrph
2		ve	. . . . . 6 setvar 𝑒
3	2	cv 1474	. . . . 5 class 𝑒
4	3	cdm 5038	. . . 4 class dom 𝑒
5		vv	. . . . . . 7 setvar 𝑣
6	5	cv 1474	. . . . . 6 class 𝑣
7	6	cpw 4108	. . . . 5 class 𝒫 𝑣
8		c0 3874	. . . . . 6 class ∅
9	8	csn 4125	. . . . 5 class {∅}
10	7, 9	cdif 3537	. . . 4 class (𝒫 𝑣 ∖ {∅})
11	4, 10, 3	wf 5800	. . 3 wff 𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})
12	11, 5, 2	copab 4642	. 2 class {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})}
13	1, 12	wceq 1475	1 wff UHGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})}

This definition is referenced by:  reluhgra  25823  isuhgra  25827  uhgrac  25834