Metamath Proof Explorer

Theorem usgredg2vtxeu

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

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

Proof

Step	Hyp	Ref	Expression
1		usgruspgr	\|- ( G e. USGraph -> G e. USPGraph )
2		uspgredg2vtxeu	\|- ( ( G e. USPGraph /\ E e. ( Edg ` G ) /\ Y e. E ) -> E! y e. ( Vtx ` G ) E = { Y , y } )
3	1 2	syl3an1	\|- ( ( G e. USGraph /\ E e. ( Edg ` G ) /\ Y e. E ) -> E! y e. ( Vtx ` G ) E = { Y , y } )

Step

Hyp

Ref

Expression

usgruspgr

 |-  ( G e. USGraph -> G e. USPGraph )

uspgredg2vtxeu

 |-  ( ( G e. USPGraph /\ E e. ( Edg ` G ) /\ Y e. E ) -> E! y e. ( Vtx ` G ) E = { Y , y } )

1 2

syl3an1

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