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

Theorem usgrav 21324
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 21322 . . 3  |-  Rel USGrph
21brrelexi 4877 . 2  |-  ( V USGrph  E  ->  V  e.  _V )
31brrelex2i 4878 . 2  |-  ( V USGrph  E  ->  E  e.  _V )
42, 3jca 519 1  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   _Vcvv 2916   class class class wbr 4172   USGrph cusg 21318
This theorem is referenced by:  usgraf  21328  usgraf0  21330  usisuslgra  21340  usgrares  21342  usgra0v  21344  usgra1v  21362  usgraedgleord  21366  fiusgraedgfi  21374  usgrafisindb0  21375  usgrafisindb1  21376  usgrares1  21377  usgrafisinds  21380  usgrafisbase  21381  nbusgra  21393  nbgrasym  21402  nbgraf1olem1  21404  cusgra2v  21424  nbcusgra  21425  cusgra3v  21426  cusgrares  21434  cusgrasize2inds  21439  cusgrafi  21444  sizeusglecusg  21448  uvtxnbgra  21455  cusgrauvtxb  21458  constr3trl  21599  constr3pth  21600  constr3cycl  21601  cusconngra  21616  vdusgraval  21631  vdgrnn0pnf  21633  hashnbgravdg  21635  usgravd0nedg  21636  usgra2pth  28041  usgra2adedgspth  28045  usgra2adedgwlk  28046  usgra2adedgwlkon  28047  usg2wlkonot  28080  usg2wotspth  28081  2pthwlkonot  28082  usg2spthonot0  28086  usg2spthonot1  28087  frgra1v  28102  frgra2v  28103  frgra3v  28106  2pthfrgra  28115  3cyclfrgrarn  28117  frconngra  28125  vdfrgra0  28126  vdgfrgra0  28127  vdgn0frgrav2  28129  vdgn1frgrav2  28131  vdgfrgragt2  28132  frgrawopreglem1  28147  frg2wot1  28160  frghash2spot  28166  usg2spot2nb  28168  usgreg2spot  28170
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-xp 4843  df-rel 4844  df-usgra 21320
  Copyright terms: Public domain W3C validator