![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1vgrex | Structured version Visualization version GIF version |
Description: A graph with at least one vertex is a set. (Contributed by AV, 2-Mar-2021.) |
Ref | Expression |
---|---|
1vgrex.v | ⊢ 𝑉 = (Vtx‘𝐺) |
Ref | Expression |
---|---|
1vgrex | ⊢ (𝑁 ∈ 𝑉 → 𝐺 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfvex 6480 | . 2 ⊢ (𝑁 ∈ (Vtx‘𝐺) → 𝐺 ∈ V) | |
2 | 1vgrex.v | . 2 ⊢ 𝑉 = (Vtx‘𝐺) | |
3 | 1, 2 | eleq2s 2877 | 1 ⊢ (𝑁 ∈ 𝑉 → 𝐺 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ∈ wcel 2107 Vcvv 3398 ‘cfv 6135 Vtxcvtx 26344 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-nul 5025 ax-pow 5077 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-dm 5365 df-iota 6099 df-fv 6143 |
This theorem is referenced by: upgr1e 26461 uspgr1e 26591 nbgrval 26683 cplgr1vlem 26777 vtxdgval 26816 vtxdgelxnn0 26820 wlkson 27003 trlsonfval 27058 pthsonfval 27092 spthson 27093 2wlkd 27316 is0wlk 27520 0wlkon 27523 is0trl 27526 0trlon 27527 0pthon 27530 0clwlkv 27534 1wlkd 27544 3wlkd 27573 wlkl0 27795 |
Copyright terms: Public domain | W3C validator |