Theorem 1vgrex 26301

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

Syntax hints:   → wi 4   = wceq 1658   ∈ wcel 2166  Vcvv 3415  ‘cfv 6124  Vtxcvtx 26295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-nul 5014  ax-pow 5066

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-dm 5353  df-iota 6087  df-fv 6132

This theorem is referenced by:  upgr1e  26412  uspgr1e  26542  nbgrval  26634  cplgr1vlem  26728  vtxdgval  26767  vtxdgelxnn0  26771  wlkson  26954  trlsonfval  27009  pthsonfval  27043  spthson  27044  2wlkd  27266  is0wlk  27494  0wlkon  27497  is0trl  27500  0trlon  27501  0pthon  27504  0clwlkv  27508  1wlkd  27518  3wlkd  27547  wlkl0  27771