Definition df-ushgra 25822

Description: Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a pair of a set and an injective (one-to-one) function into the powerset of this set (the empty set excluded). (Contributed by AV, 19-Jan-2020.)

Assertion

Ref	Expression
df-ushgra	⊢ USHGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})}

Distinct variable group:   𝑣,𝑒

Detailed syntax breakdown of Definition df-ushgra

Step	Hyp	Ref	Expression
1		cushg 25820	. 2 class USHGrph
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	wf1 5801	. . 3 wff 𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})
12	11, 5, 2	copab 4642	. 2 class {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})}
13	1, 12	wceq 1475	1 wff USHGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})}

This definition is referenced by:  relushgra  25824  isushgra  25830