Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 uspgrloopvtx.g G = V A N
2 1 uspgrloopvtx V W Vtx G = V
3 eleq2 V = Vtx G N V N Vtx G
4 3 biimpd V = Vtx G N V N Vtx G
5 4 eqcoms Vtx G = V N V N Vtx G
6 5 com12 N V Vtx G = V N Vtx G
7 2 6 mpan9 V W N V N Vtx G