Theorem usgredg2vtx

Description: For a vertex incident to an edge there is another vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020) (Proof shortened by AV, 5-Dec-2020)

	Ref	Expression
Assertion	usgredg2vtx	|- ( ( G e. USGraph /\ E e. ( Edg ` G ) /\ Y e. E ) -> E. y e. ( Vtx ` G ) E = { Y , y } )

Proof

Step	Hyp	Ref	Expression
1		usgrupgr	|- ( G e. USGraph -> G e. UPGraph )
2		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
3		eqid	|- ( Edg ` G ) = ( Edg ` G )
4	2 3	upgredg2vtx	|- ( ( G e. UPGraph /\ E e. ( Edg ` G ) /\ Y e. E ) -> E. y e. ( Vtx ` G ) E = { Y , y } )
5	1 4	syl3an1	|- ( ( G e. USGraph /\ E e. ( Edg ` G ) /\ Y e. E ) -> E. y e. ( Vtx ` G ) E = { Y , y } )