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 e. W /\ N e. V ) -> N e. ( Vtx ` G ) )

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	|- G = <. V , { <. A , { N } >. } >.
2	1	uspgrloopvtx	|- ( V e. W -> ( Vtx ` G ) = V )
3		eleq2	|- ( V = ( Vtx ` G ) -> ( N e. V <-> N e. ( Vtx ` G ) ) )
4	3	biimpd	|- ( V = ( Vtx ` G ) -> ( N e. V -> N e. ( Vtx ` G ) ) )
5	4	eqcoms	|- ( ( Vtx ` G ) = V -> ( N e. V -> N e. ( Vtx ` G ) ) )
6	5	com12	|- ( N e. V -> ( ( Vtx ` G ) = V -> N e. ( Vtx ` G ) ) )
7	2 6	mpan9	|- ( ( V e. W /\ N e. V ) -> N e. ( Vtx ` G ) )