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

Theorem usgrav 23292
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 23290 . . 3  |-  Rel USGrph
21brrelexi 4900 . 2  |-  ( V USGrph  E  ->  V  e.  _V )
31brrelex2i 4901 . 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 1756   _Vcvv 2993   class class class wbr 4313   USGrph cusg 23286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314  df-opab 4372  df-xp 4867  df-rel 4868  df-usgra 23288
This theorem is referenced by:  usgraf  23296  usgraf0  23298  usisuslgra  23308  usgrares  23310  usgra0v  23312  usgra1v  23330  usgraedgleord  23334  fiusgraedgfi  23342  usgrafisindb0  23343  usgrafisindb1  23344  usgrares1  23345  usgrafisinds  23348  usgrafisbase  23349  nbusgra  23361  nbgrasym  23370  nbgraf1olem1  23372  cusgra2v  23392  nbcusgra  23393  cusgra3v  23394  cusgrares  23402  cusgrasize2inds  23407  cusgrafi  23412  sizeusglecusg  23416  uvtxnbgra  23423  cusgrauvtxb  23426  constr3trl  23567  constr3pth  23568  constr3cycl  23569  cusconngra  23584  vdusgraval  23599  vdgrnn0pnf  23601  hashnbgravdg  23603  usgravd0nedg  23604  uvtxnb  30304  usgra2pth  30327  usgra2adedgspth  30331  usgra2adedgwlk  30332  usgra2adedgwlkon  30333  usg2wlkonot  30428  usg2wotspth  30429  2pthwlkonot  30430  usg2spthonot0  30434  usg2spthonot1  30435  clwwlkgt0  30460  clwwlkn0  30463  clwwlkn2  30464  clwlkisclwwlk  30477  hashclwwlkn  30536  clwwlkndivn  30537  clwlkfclwwlk  30543  cusgraisrusgra  30577  0eusgraiff0rgra  30578  rusgraprop3  30581  rusgrasn  30583  rusgranumwlkl1lem1  30584  rusgranumwlkl1  30585  rusgranumwlkb0  30597  rusgra0edg  30599  frgra1v  30616  frgra2v  30617  frgra3v  30620  2pthfrgra  30629  3cyclfrgrarn  30631  frconngra  30639  vdfrgra0  30640  vdgfrgra0  30641  vdgn0frgrav2  30643  vdgn1frgrav2  30645  vdgfrgragt2  30646  frgrawopreglem1  30663  frg2wot1  30676  frghash2spot  30682  usg2spot2nb  30684  usgreg2spot  30686  frgraregorufrg  30691  extwwlkfablem1  30693  extwwlkfablem2  30697  numclwwlkovfel2  30702  numclwwlkovf2ex  30705  numclwwlkovgelim  30708  numclwwlk1  30717  numclwwlkqhash  30719  numclwwlk3lem  30727  numclwwlk3  30728  numclwwlk4  30729  numclwwlk5  30731  numclwwlk6  30732  frgrareg  30736
  Copyright terms: Public domain W3C validator