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

Theorem usgrav 23093
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 23091 . . 3  |-  Rel USGrph
21brrelexi 4866 . 2  |-  ( V USGrph  E  ->  V  e.  _V )
31brrelex2i 4867 . 2  |-  ( V USGrph  E  ->  E  e.  _V )
42, 3jca 529 1  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1755   _Vcvv 2962   class class class wbr 4280   USGrph cusg 23087
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-xp 4833  df-rel 4834  df-usgra 23089
This theorem is referenced by:  usgraf  23097  usgraf0  23099  usisuslgra  23109  usgrares  23111  usgra0v  23113  usgra1v  23131  usgraedgleord  23135  fiusgraedgfi  23143  usgrafisindb0  23144  usgrafisindb1  23145  usgrares1  23146  usgrafisinds  23149  usgrafisbase  23150  nbusgra  23162  nbgrasym  23171  nbgraf1olem1  23173  cusgra2v  23193  nbcusgra  23194  cusgra3v  23195  cusgrares  23203  cusgrasize2inds  23208  cusgrafi  23213  sizeusglecusg  23217  uvtxnbgra  23224  cusgrauvtxb  23227  constr3trl  23368  constr3pth  23369  constr3cycl  23370  cusconngra  23385  vdusgraval  23400  vdgrnn0pnf  23402  hashnbgravdg  23404  usgravd0nedg  23405  uvtxnb  30124  usgra2pth  30147  usgra2adedgspth  30151  usgra2adedgwlk  30152  usgra2adedgwlkon  30153  usg2wlkonot  30248  usg2wotspth  30249  2pthwlkonot  30250  usg2spthonot0  30254  usg2spthonot1  30255  clwwlkgt0  30280  clwwlkn0  30283  clwwlkn2  30284  clwlkisclwwlk  30297  hashclwwlkn  30356  clwwlkndivn  30357  clwlkfclwwlk  30363  cusgraisrusgra  30397  0eusgraiff0rgra  30398  rusgraprop3  30401  rusgrasn  30403  rusgranumwlkl1lem1  30404  rusgranumwlkl1  30405  rusgranumwlkb0  30417  rusgra0edg  30419  frgra1v  30436  frgra2v  30437  frgra3v  30440  2pthfrgra  30449  3cyclfrgrarn  30451  frconngra  30459  vdfrgra0  30460  vdgfrgra0  30461  vdgn0frgrav2  30463  vdgn1frgrav2  30465  vdgfrgragt2  30466  frgrawopreglem1  30483  frg2wot1  30496  frghash2spot  30502  usg2spot2nb  30504  usgreg2spot  30506  frgraregorufrg  30511  extwwlkfablem1  30513  extwwlkfablem2  30517  numclwwlkovfel2  30522  numclwwlkovf2ex  30525  numclwwlkovgelim  30528  numclwwlk1  30537  numclwwlkqhash  30539  numclwwlk3lem  30547  numclwwlk3  30548  numclwwlk4  30549  numclwwlk5  30551  numclwwlk6  30552  frgrareg  30556
  Copyright terms: Public domain W3C validator