Theorem uspgrloopvtxel

Description: A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop ). (Contributed by AV, 17-Dec-2020)

	Ref	Expression
Hypothesis	uspgrloopvtx.g	⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
Assertion	uspgrloopvtxel	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
2	1	uspgrloopvtx	⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 )
3		eleq2	⊢ ( 𝑉 = ( Vtx ‘ 𝐺 ) → ( 𝑁 ∈ 𝑉 ↔ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
4	3	biimpd	⊢ ( 𝑉 = ( Vtx ‘ 𝐺 ) → ( 𝑁 ∈ 𝑉 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
5	4	eqcoms	⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( 𝑁 ∈ 𝑉 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
6	5	com12	⊢ ( 𝑁 ∈ 𝑉 → ( ( Vtx ‘ 𝐺 ) = 𝑉 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
7	2 6	mpan9	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )