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

Theorem usgrav 25114
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 25111 . . 3  |-  Rel USGrph
21brrelexi 4894 . 2  |-  ( V USGrph  E  ->  V  e.  _V )
31brrelex2i 4895 . 2  |-  ( V USGrph  E  ->  E  e.  _V )
42, 3jca 539 1  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1898   _Vcvv 3057   class class class wbr 4416   USGrph cusg 25106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-opab 4476  df-xp 4859  df-rel 4860  df-usgra 25109
This theorem is referenced by:  usgraf  25122  usgraf0  25124  usisuslgra  25141  usgrares  25145  usgra0v  25147  usgra1v  25166  usgraedgleord  25170  fiusgraedgfi  25184  usgrafisindb0  25185  usgrafisindb1  25186  usgrares1  25187  usgrafisinds  25190  usgrafisbase  25191  nbusgra  25205  nbgrasym  25216  nbgraf1olem1  25218  cusgra2v  25239  nbcusgra  25240  cusgra3v  25241  cusgrares  25249  cusgrasize2inds  25254  cusgrafi  25259  sizeusglecusg  25263  uvtxnbgra  25270  cusgrauvtxb  25273  uvtxnb  25274  usgra2adedgspth  25390  usgra2adedgwlk  25391  usgra2adedgwlkon  25392  constr3trl  25436  constr3pth  25437  constr3cycl  25438  cusconngra  25453  clwwlkgt0  25548  clwwlkn0  25551  clwwlkn2  25552  clwlkisclwwlk  25566  hashclwwlkn  25613  clwwlkndivn  25614  clwlkfclwwlk  25621  usg2wlkonot  25660  usg2wotspth  25661  2pthwlkonot  25662  usg2spthonot0  25666  usg2spthonot1  25667  vdusgraval  25684  vdgrnn0pnf  25686  hashnbgravdg  25690  usgravd0nedg  25695  cusgraisrusgra  25715  0eusgraiff0rgra  25716  rusgraprop3  25720  rusgrasn  25722  rusgranumwwlkl1  25723  rusgranumwlkl1  25724  rusgranumwlkb0  25730  rusgra0edg  25732  frgra1v  25775  frgra2v  25776  frgra3v  25779  2pthfrgra  25788  3cyclfrgrarn  25790  frconngra  25798  vdfrgra0  25799  vdgn0frgrav2  25801  vdgn1frgrav2  25803  vdgfrgragt2  25804  frgrawopreglem1  25821  frg2wot1  25834  frghash2spot  25840  usg2spot2nb  25842  usgreg2spot  25844  frgraregorufrg  25849  extwwlkfablem1  25851  extwwlkfablem2  25855  numclwwlkovfel2  25860  numclwwlkovf2ex  25863  numclwwlkovgelim  25866  numclwwlk1  25875  numclwwlkqhash  25877  numclwwlk3lem  25885  numclwwlk3  25886  numclwwlk4  25887  numclwwlk5  25889  numclwwlk6  25890  frgrareg  25894  usgra2pth  39941  usgedgffibi  40019  usgrafisbaseALT  40025  usgrafisbaseALT2  40026  usgfis  40031  usgfisALT  40035
  Copyright terms: Public domain W3C validator