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 \in W \to Vtx (G) = V$

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\}⟩\} \in V$
4		opvtxfv	$⊢ (V \in W \land \{⟨0, \{A, B\}⟩, ⟨1, \{A, B\}⟩\} \in V) \to Vtx (⟨V, \{⟨0, \{A, B\}⟩, ⟨1, \{A, B\}⟩\}⟩) = V$
5	3 4	mpan2	$⊢ V \in W \to Vtx (⟨V, \{⟨0, \{A, B\}⟩, ⟨1, \{A, B\}⟩\}⟩) = V$
6	2 5	eqtrid	$⊢ V \in W \to Vtx (G) = V$

Metamath Proof Explorer