Metamath Proof Explorer
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 |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ) → 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
uhgredgn0 |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ) → 𝐸 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) |
| 2 |
1
|
eldifad |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ) → 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ) |