Theorem umgr2v2evtxel

Description: A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020)

	Ref	Expression
Hypothesis	umgr2v2evtx.g	|- G = <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >.
Assertion	umgr2v2evtxel	|- ( ( V e. W /\ A e. V ) -> A e. ( Vtx ` G ) )

Proof

Step	Hyp	Ref	Expression
1		umgr2v2evtx.g	|- G = <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >.
2	1	umgr2v2evtx	|- ( V e. W -> ( Vtx ` G ) = V )
3		eqcom	|- ( ( Vtx ` G ) = V <-> V = ( Vtx ` G ) )
4	3	biimpi	|- ( ( Vtx ` G ) = V -> V = ( Vtx ` G ) )
5	4	eleq2d	|- ( ( Vtx ` G ) = V -> ( A e. V <-> A e. ( Vtx ` G ) ) )
6	5	biimpcd	|- ( A e. V -> ( ( Vtx ` G ) = V -> A e. ( Vtx ` G ) ) )
7	2 6	mpan9	|- ( ( V e. W /\ A e. V ) -> A e. ( Vtx ` G ) )