Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rusisusgra Structured version   Unicode version

Theorem rusisusgra 30689
 Description: Any k-regular undirected simple graph is an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
Assertion
Ref Expression
rusisusgra RegUSGrph USGrph

Proof of Theorem rusisusgra
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 rusgraprop 30687 . 2 RegUSGrph USGrph VDeg
21simp1d 1000 1 RegUSGrph USGrph
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1370   wcel 1758  wral 2795  cop 3984   class class class wbr 4393  cfv 5519  (class class class)co 6193  cn0 10683   USGrph cusg 23409   VDeg cvdg 23708   RegUSGrph crusgra 30681 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-xp 4947  df-rel 4948  df-iota 5482  df-fv 5527  df-ov 6196  df-oprab 6197  df-rgra 30682  df-rusgra 30683 This theorem is referenced by:  rusgranumwlkl1lem1  30699  rusgranumwlkl1  30700  rusgranumwlkb1  30713  rusgra0edg  30714  rusgranumwlks  30715  rusgranumwlk  30716  rusgranumwwlkg  30718  numclwwlkovf2num  30819  numclwwlk1  30832  numclwwlkqhash  30834  numclwwlk3  30843  numclwwlk5  30846  numclwwlk6  30847  frgrareg  30851
 Copyright terms: Public domain W3C validator