Theorem uspgrloopvtx

Description: The set of vertices 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	uspgrloopvtx	⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
2	1	fveq2i	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩ )
3		snex	⊢ { ⟨ 𝐴 , { 𝑁 } ⟩ } ∈ V
4		opvtxfv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ { ⟨ 𝐴 , { 𝑁 } ⟩ } ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩ ) = 𝑉 )
5	3 4	mpan2	⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩ ) = 𝑉 )
6	2 5	syl5eq	⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 )