Metamath Proof Explorer

Theorem edguhgr

Description: An edge of a hypergraph is a subset of vertices. (Contributed by AV, 26-Oct-2020) (Proof shortened by AV, 28-Nov-2020)

Ref Expression
Assertion edguhgr ⊢ G ∈ UHGraph ∧ E ∈ Edg ⁡ G → E ∈ 𝒫 Vtx ⁡ G

Proof

Step Hyp Ref Expression
1 uhgredgn0 ⊢ G ∈ UHGraph ∧ E ∈ Edg ⁡ G → E ∈ 𝒫 Vtx ⁡ G ∖ ∅
2 1 eldifad ⊢ G ∈ UHGraph ∧ E ∈ Edg ⁡ G → E ∈ 𝒫 Vtx ⁡ G