Theorem 1vgrex 29585

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

Hypothesis

Ref	Expression
1vgrex.v	⊢ 𝑉 = (Vtx‘𝐺)

Assertion

Ref	Expression
1vgrex	⊢ (𝑁 ∈ 𝑉 → 𝐺 ∈ V)

Proof of Theorem 1vgrex

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ‘cfv 6538  Vtxcvtx 29579

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-dm 5660  df-iota 6494  df-fv 6546

This theorem is used by:  upgr1e  29696  uspgr1e  29830  nbgrval  29922  cplgr1vlem  30015  vtxdgval  30054  vtxdgelxnn0  30058  wlkson  30240  trlsonfval  30293  pthsonfval  30331  spthson  30332  2wlkd  30530  is0wlk  30713  0wlkon  30716  is0trl  30719  0trlon  30720  0pthon  30723  0clwlkv  30727  1wlkd  30737  3wlkd  30776  wlkl0  30973  clnbgrval  49013  isgrtri  49134