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 ‘ 𝐺 ) )