Metamath Proof Explorer

Theorem opvtxval

Description: The set of vertices of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 9-Jan-2020) (Revised by AV, 21-Sep-2020)

		Ref	Expression
	Assertion	opvtxval	⊢ ( 𝐺 ∈ ( V × V ) → ( Vtx ‘ 𝐺 ) = ( 1^st ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		vtxval	⊢ ( Vtx ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 1^st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) )
2		iftrue	⊢ ( 𝐺 ∈ ( V × V ) → if ( 𝐺 ∈ ( V × V ) , ( 1^st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) ) = ( 1^st ‘ 𝐺 ) )
3	1 2	syl5eq	⊢ ( 𝐺 ∈ ( V × V ) → ( Vtx ‘ 𝐺 ) = ( 1^st ‘ 𝐺 ) )