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=\mathrm{Vtx}\left(G\right)$$
	edgssv2.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	usgredg	$$⊢\left(G\in \mathrm{USGraph}\wedge C\in E\right)\to \exists a\in V\exists b\in V\left(a\ne b\wedge C=\left\{a,b\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		edgssv2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		edgssv2.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3		usgrumgr	$$⊢G\in \mathrm{USGraph}\to G\in \mathrm{UMGraph}$$
4	1 2	umgredg	$$⊢\left(G\in \mathrm{UMGraph}\wedge C\in E\right)\to \exists a\in V\exists b\in V\left(a\ne b\wedge C=\left\{a,b\right\}\right)$$
5	3 4	sylan	$$⊢\left(G\in \mathrm{USGraph}\wedge C\in E\right)\to \exists a\in V\exists b\in V\left(a\ne b\wedge C=\left\{a,b\right\}\right)$$