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

Step	Hyp	Ref	Expression
1		uhgredgn0	\|- ( ( G e. UHGraph /\ x e. ( Edg ` G ) ) -> x e. ( ~P ( Vtx ` G ) \ { (/) } ) )
2	1	ex	\|- ( G e. UHGraph -> ( x e. ( Edg ` G ) -> x e. ( ~P ( Vtx ` G ) \ { (/) } ) ) )
3	2	ssrdv	\|- ( G e. UHGraph -> ( Edg ` G ) C_ ( ~P ( Vtx ` G ) \ { (/) } ) )

Step

Hyp

Ref

Expression

 |-  ( ( G e. UHGraph /\ x e. ( Edg ` G ) ) -> x e. ( ~P ( Vtx ` G ) \ { (/) } ) )

 |-  ( G e. UHGraph -> ( x e. ( Edg ` G ) -> x e. ( ~P ( Vtx ` G ) \ { (/) } ) ) )

 |-  ( G e. UHGraph -> ( Edg ` G ) C_ ( ~P ( Vtx ` G ) \ { (/) } ) )