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 e. V -> G e. _V )

Proof

Step Hyp Ref Expression
1 1vgrex.v 
 |-  V = ( Vtx ` G )
2 elfvex 
 |-  ( N e. ( Vtx ` G ) -> G e. _V )
3 2 1 eleq2s 
 |-  ( N e. V -> G e. _V )