Metamath Proof Explorer


Theorem umgr2v2evtxel

Description: A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
Assertion umgr2v2evtxel ( ( 𝑉𝑊𝐴𝑉 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
2 1 umgr2v2evtx ( 𝑉𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 )
3 eqcom ( ( Vtx ‘ 𝐺 ) = 𝑉𝑉 = ( Vtx ‘ 𝐺 ) )
4 3 biimpi ( ( Vtx ‘ 𝐺 ) = 𝑉𝑉 = ( Vtx ‘ 𝐺 ) )
5 4 eleq2d ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( 𝐴𝑉𝐴 ∈ ( Vtx ‘ 𝐺 ) ) )
6 5 biimpcd ( 𝐴𝑉 → ( ( Vtx ‘ 𝐺 ) = 𝑉𝐴 ∈ ( Vtx ‘ 𝐺 ) ) )
7 2 6 mpan9 ( ( 𝑉𝑊𝐴𝑉 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )