Theorem 1vgrex

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

	Ref	Expression
Hypothesis	1vgrex.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	1vgrex	⊢ ( 𝑁 ∈ 𝑉 → 𝐺 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		1vgrex.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		elfvex	⊢ ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) → 𝐺 ∈ V )
3	2 1	eleq2s	⊢ ( 𝑁 ∈ 𝑉 → 𝐺 ∈ V )