Metamath Proof Explorer

Theorem uhgredgrnv

Description: An edge of a hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 4-Jun-2021)

Ref Expression
Assertion uhgredgrnv ⊢G∈UHGraph∧E∈Edg⁡G∧N∈E→N∈Vtx⁡G

Proof

Step Hyp Ref Expression
1 edguhgr ⊢G∈UHGraph∧E∈Edg⁡G→E∈𝒫Vtx⁡G
2 elelpwi ⊢N∈E∧E∈𝒫Vtx⁡G→N∈Vtx⁡G
3 2 expcom ⊢E∈𝒫Vtx⁡G→N∈E→N∈Vtx⁡G
4 1 3 syl ⊢G∈UHGraph∧E∈Edg⁡G→N∈E→N∈Vtx⁡G
5 4 3impia ⊢G∈UHGraph∧E∈Edg⁡G∧N∈E→N∈Vtx⁡G