This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uhgredgss

Description: The set of edges of a hypergraph is a subset of the power set of vertices without the empty set. (Contributed by AV, 29-Nov-2020)

Ref Expression
Assertion uhgredgss ⊢ G ∈ UHGraph → Edg ⁡ G ⊆ 𝒫 Vtx ⁡ G ∖ ∅

Proof

Step Hyp Ref Expression
1 uhgredgn0 ⊢ G ∈ UHGraph ∧ x ∈ Edg ⁡ G → x ∈ 𝒫 Vtx ⁡ G ∖ ∅
2 1 ex ⊢ G ∈ UHGraph → x ∈ Edg ⁡ G → x ∈ 𝒫 Vtx ⁡ G ∖ ∅
3 2 ssrdv ⊢ G ∈ UHGraph → Edg ⁡ G ⊆ 𝒫 Vtx ⁡ G ∖ ∅