Theorem 1vgrex 29090

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ‘cfv 6490  Vtxcvtx 29084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-dm 5632  df-iota 6446  df-fv 6498

This theorem is referenced by:  upgr1e  29201  uspgr1e  29332  nbgrval  29424  cplgr1vlem  29517  vtxdgval  29557  vtxdgelxnn0  29561  wlkson  29743  trlsonfval  29792  pthsonfval  29828  spthson  29829  2wlkd  30024  is0wlk  30207  0wlkon  30210  is0trl  30213  0trlon  30214  0pthon  30217  0clwlkv  30221  1wlkd  30231  3wlkd  30260  wlkl0  30457  clnbgrval  48295  isgrtri  48416