Theorem 1vgrex 29138

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 6887	. 2 ⊢ (𝑁 ∈ (Vtx‘𝐺) → 𝐺 ∈ V)
2		1vgrex.v	. 2 ⊢ 𝑉 = (Vtx‘𝐺)
3	1, 2	eleq2s 2870	1 ⊢ (𝑁 ∈ 𝑉 → 𝐺 ∈ V)

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132  Vcvv 3444  ‘cfv 6506  Vtxcvtx 29132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-nul 5246  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-ne 2948  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-dm 5646  df-iota 6462  df-fv 6514

This theorem is referenced by:  upgr1e  29249  uspgr1e  29380  nbgrval  29472  cplgr1vlem  29565  vtxdgval  29604  vtxdgelxnn0  29608  wlkson  29790  trlsonfval  29839  pthsonfval  29875  spthson  29876  2wlkd  30071  is0wlk  30254  0wlkon  30257  is0trl  30260  0trlon  30261  0pthon  30264  0clwlkv  30268  1wlkd  30278  3wlkd  30307  wlkl0  30504  clnbgrval  48382  isgrtri  48503