This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1vgrex

Description: A graph with at least one vertex is a set. (Contributed by AV, 2-Mar-2021)

		Ref	Expression
	Hypothesis	1vgrex.v	$⊢ V = Vtx (G)$
	Assertion	1vgrex	$⊢ N \in V \to G \in V$

Step	Hyp	Ref	Expression
1		1vgrex.v	$⊢ V = Vtx (G)$
2		elfvex	$⊢ N \in Vtx (G) \to G \in V$
3	2 1	eleq2s	$⊢ N \in V \to G \in V$