Theorem uhgrss

Description: An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017) (Revised by AV, 18-Jan-2020)

	Ref	Expression
Hypotheses	uhgrf.v	|- V = ( Vtx ` G )
	uhgrf.e	|- E = ( iEdg ` G )
Assertion	uhgrss	|- ( ( G e. UHGraph /\ F e. dom E ) -> ( E ` F ) C_ V )

Proof

Step	Hyp	Ref	Expression
1		uhgrf.v	|- V = ( Vtx ` G )
2		uhgrf.e	|- E = ( iEdg ` G )
3	1 2	uhgrf	|- ( G e. UHGraph -> E : dom E --> ( ~P V \ { (/) } ) )
4	3	ffvelcdmda	|- ( ( G e. UHGraph /\ F e. dom E ) -> ( E ` F ) e. ( ~P V \ { (/) } ) )
5	4	eldifad	|- ( ( G e. UHGraph /\ F e. dom E ) -> ( E ` F ) e. ~P V )
6	5	elpwid	|- ( ( G e. UHGraph /\ F e. dom E ) -> ( E ` F ) C_ V )