MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  usgrav Structured version   Unicode version

Theorem usgrav 24316
Description: The classes of vertices and edges of an undirected simple graph without loops are sets. (Contributed by Alexander van der Vekens, 19-Aug-2017.)
Assertion
Ref Expression
usgrav  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )

Proof of Theorem usgrav
StepHypRef Expression
1 relusgra 24313 . . 3  |-  Rel USGrph
21brrelexi 5030 . 2  |-  ( V USGrph  E  ->  V  e.  _V )
31brrelex2i 5031 . 2  |-  ( V USGrph  E  ->  E  e.  _V )
42, 3jca 532 1  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1804   _Vcvv 3095   class class class wbr 4437   USGrph cusg 24308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-xp 4995  df-rel 4996  df-usgra 24311
This theorem is referenced by:  usgraf  24324  usgraf0  24326  usisuslgra  24343  usgrares  24347  usgra0v  24349  usgra1v  24368  usgraedgleord  24372  fiusgraedgfi  24385  usgrafisindb0  24386  usgrafisindb1  24387  usgrares1  24388  usgrafisinds  24391  usgrafisbase  24392  nbusgra  24406  nbgrasym  24417  nbgraf1olem1  24419  cusgra2v  24440  nbcusgra  24441  cusgra3v  24442  cusgrares  24450  cusgrasize2inds  24455  cusgrafi  24460  sizeusglecusg  24464  uvtxnbgra  24471  cusgrauvtxb  24474  uvtxnb  24475  usgra2adedgspth  24591  usgra2adedgwlk  24592  usgra2adedgwlkon  24593  constr3trl  24637  constr3pth  24638  constr3cycl  24639  cusconngra  24654  clwwlkgt0  24749  clwwlkn0  24752  clwwlkn2  24753  clwlkisclwwlk  24767  hashclwwlkn  24814  clwwlkndivn  24815  clwlkfclwwlk  24822  usg2wlkonot  24861  usg2wotspth  24862  2pthwlkonot  24863  usg2spthonot0  24867  usg2spthonot1  24868  vdusgraval  24885  vdgrnn0pnf  24887  hashnbgravdg  24891  usgravd0nedg  24896  cusgraisrusgra  24916  0eusgraiff0rgra  24917  rusgraprop3  24921  rusgrasn  24923  rusgranumwwlkl1  24924  rusgranumwlkl1  24925  rusgranumwlkb0  24931  rusgra0edg  24933  frgra1v  24976  frgra2v  24977  frgra3v  24980  2pthfrgra  24989  3cyclfrgrarn  24991  frconngra  24999  vdfrgra0  25000  vdgn0frgrav2  25002  vdgn1frgrav2  25004  vdgfrgragt2  25005  frgrawopreglem1  25022  frg2wot1  25035  frghash2spot  25041  usg2spot2nb  25043  usgreg2spot  25045  frgraregorufrg  25050  extwwlkfablem1  25052  extwwlkfablem2  25056  numclwwlkovfel2  25061  numclwwlkovf2ex  25064  numclwwlkovgelim  25067  numclwwlk1  25076  numclwwlkqhash  25078  numclwwlk3lem  25086  numclwwlk3  25087  numclwwlk4  25088  numclwwlk5  25090  numclwwlk6  25091  frgrareg  25095  usgra2pth  32308  usgedgffibi  32388  usgrafisbaseALT  32394  usgrafisbaseALT2  32395  usgfis  32400  usgfisALT  32404
  Copyright terms: Public domain W3C validator