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

Theorem usgrav 24003
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 24000 . . 3  |-  Rel USGrph
21brrelexi 5034 . 2  |-  ( V USGrph  E  ->  V  e.  _V )
31brrelex2i 5035 . 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 1762   _Vcvv 3108   class class class wbr 4442   USGrph cusg 23995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pr 4681
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-br 4443  df-opab 4501  df-xp 5000  df-rel 5001  df-usgra 23998
This theorem is referenced by:  usgraf  24011  usgraf0  24013  usisuslgra  24029  usgrares  24033  usgra0v  24035  usgra1v  24054  usgraedgleord  24058  fiusgraedgfi  24071  usgrafisindb0  24072  usgrafisindb1  24073  usgrares1  24074  usgrafisinds  24077  usgrafisbase  24078  nbusgra  24092  nbgrasym  24103  nbgraf1olem1  24105  cusgra2v  24126  nbcusgra  24127  cusgra3v  24128  cusgrares  24136  cusgrasize2inds  24141  cusgrafi  24146  sizeusglecusg  24150  uvtxnbgra  24157  cusgrauvtxb  24160  uvtxnb  24161  usgra2adedgspth  24277  usgra2adedgwlk  24278  usgra2adedgwlkon  24279  constr3trl  24323  constr3pth  24324  constr3cycl  24325  cusconngra  24340  clwwlkgt0  24435  clwwlkn0  24438  clwwlkn2  24439  clwlkisclwwlk  24453  hashclwwlkn  24500  clwwlkndivn  24501  clwlkfclwwlk  24508  usg2wlkonot  24547  usg2wotspth  24548  2pthwlkonot  24549  usg2spthonot0  24553  usg2spthonot1  24554  vdusgraval  24571  vdgrnn0pnf  24573  hashnbgravdg  24577  usgravd0nedg  24582  cusgraisrusgra  24602  0eusgraiff0rgra  24603  rusgraprop3  24607  rusgrasn  24609  rusgranumwwlkl1  24610  rusgranumwlkl1  24611  rusgranumwlkb0  24617  rusgra0edg  24619  frgra1v  24662  frgra2v  24663  frgra3v  24666  2pthfrgra  24675  3cyclfrgrarn  24677  frconngra  24685  vdfrgra0  24686  vdgfrgra0  24687  vdgn0frgrav2  24689  vdgn1frgrav2  24691  vdgfrgragt2  24692  frgrawopreglem1  24709  frg2wot1  24722  frghash2spot  24728  usg2spot2nb  24730  usgreg2spot  24732  frgraregorufrg  24737  extwwlkfablem1  24739  extwwlkfablem2  24743  numclwwlkovfel2  24748  numclwwlkovf2ex  24751  numclwwlkovgelim  24754  numclwwlk1  24763  numclwwlkqhash  24765  numclwwlk3lem  24773  numclwwlk3  24774  numclwwlk4  24775  numclwwlk5  24777  numclwwlk6  24778  frgrareg  24782  usgra2pth  31780  usgedgffibi  31834  usgrafisbaseALT  31837  usgfis  31842
  Copyright terms: Public domain W3C validator