Theorem usgredg

Description: For each edge in a simple graph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017) (Revised by AV, 17-Oct-2020) (Shortened by AV, 25-Nov-2020.)

	Ref	Expression
Hypotheses	edgssv2.v	|- V = ( Vtx ` G )
	edgssv2.e	|- E = ( Edg ` G )
Assertion	usgredg	|- ( ( G e. USGraph /\ C e. E ) -> E. a e. V E. b e. V ( a =/= b /\ C = { a , b } ) )

Proof

Step	Hyp	Ref	Expression
1		edgssv2.v	|- V = ( Vtx ` G )
2		edgssv2.e	|- E = ( Edg ` G )
3		usgrumgr	|- ( G e. USGraph -> G e. UMGraph )
4	1 2	umgredg	|- ( ( G e. UMGraph /\ C e. E ) -> E. a e. V E. b e. V ( a =/= b /\ C = { a , b } ) )
5	3 4	sylan	|- ( ( G e. USGraph /\ C e. E ) -> E. a e. V E. b e. V ( a =/= b /\ C = { a , b } ) )