This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgredgne

Description: An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv resp. usgrnloop . (Contributed by Alexander van der Vekens, 2-Sep-2017) (Revised by AV, 17-Oct-2020) (Proof shortened by AV, 27-Nov-2020)

		Ref	Expression
	Hypothesis	usgredgne.v	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	Assertion	usgredgne	⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → 𝑀 ≠ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		usgredgne.v	⊢ 𝐸 = ( Edg ‘ 𝐺 )
2		usgrumgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
3	1	umgredgne	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → 𝑀 ≠ 𝑁 )
4	2 3	sylan	⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → 𝑀 ≠ 𝑁 )