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 e. UHGraph /\ E e. ( Edg ` G ) ) -> E e. ~P ( Vtx ` G ) )

Proof

Step Hyp Ref Expression
1 uhgredgn0 
 |-  ( ( G e. UHGraph /\ E e. ( Edg ` G ) ) -> E e. ( ~P ( Vtx ` G ) \ { (/) } ) )
2 1 eldifad 
 |-  ( ( G e. UHGraph /\ E e. ( Edg ` G ) ) -> E e. ~P ( Vtx ` G ) )