Metamath Proof Explorer


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 G = V A N
Assertion uspgrloopvtx V W Vtx G = V

Proof

Step Hyp Ref Expression
1 uspgrloopvtx.g G = V A N
2 1 fveq2i Vtx G = Vtx V A N
3 snex A N V
4 opvtxfv V W A N V Vtx V A N = V
5 3 4 mpan2 V W Vtx V A N = V
6 2 5 syl5eq V W Vtx G = V