Metamath Proof Explorer

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 ∈ USGraph ∧ C ∈ E → ∃ a ∈ V ∃ b ∈ 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 ∈ USGraph → G ∈ UMGraph
4 1 2 umgredg ⊢ G ∈ UMGraph ∧ C ∈ E → ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ C = a b
5 3 4 sylan ⊢ G ∈ USGraph ∧ C ∈ E → ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ C = a b