MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1vgrex Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 elfvex 6468 . 2 (𝑁 ∈ (Vtx‘𝐺) → 𝐺 ∈ V)
2 1vgrex.v . 2 𝑉 = (Vtx‘𝐺)
31, 2eleq2s 2925 1 (𝑁𝑉𝐺 ∈ V)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator