Theorem umgr2v2evtx

Description: The set of vertices 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	umgr2v2evtx	|- ( V e. W -> ( Vtx ` G ) = V )

Proof

Step	Hyp	Ref	Expression
1		umgr2v2evtx.g	|- G = <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >.
2	1	fveq2i	|- ( Vtx ` G ) = ( Vtx ` <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >. )
3		prex	|- { <. 0 , { A , B } >. , <. 1 , { A , B } >. } e. _V
4		opvtxfv	|- ( ( V e. W /\ { <. 0 , { A , B } >. , <. 1 , { A , B } >. } e. _V ) -> ( Vtx ` <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >. ) = V )
5	3 4	mpan2	|- ( V e. W -> ( Vtx ` <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >. ) = V )
6	2 5	syl5eq	|- ( V e. W -> ( Vtx ` G ) = V )