Theorem usgrss

Description: An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 15-Oct-2020)

	Ref	Expression
Hypotheses	usgrf1o.e	|- E = ( iEdg ` G )
	usgrss.v	|- V = ( Vtx ` G )
Assertion	usgrss	|- ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) C_ V )

Proof

Step	Hyp	Ref	Expression
1		usgrf1o.e	|- E = ( iEdg ` G )
2		usgrss.v	|- V = ( Vtx ` G )
3		ssrab2	|- { x e. ~P V | ( # ` x ) = 2 } C_ ~P V
4	2 1	usgrfs	|- ( G e. USGraph -> E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } )
5		f1f	|- ( E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } -> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } )
6	4 5	syl	|- ( G e. USGraph -> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } )
7	6	ffvelrnda	|- ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) e. { x e. ~P V | ( # ` x ) = 2 } )
8	3 7	sseldi	|- ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) e. ~P V )
9	8	elpwid	|- ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) C_ V )