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

Theorem rusgrargra 30688
 Description: A k-regular undirected simple graph is a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
Assertion
Ref Expression
rusgrargra RegUSGrph RegGrph

Proof of Theorem rusgrargra
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-rusgra 30683 . . . 4 RegUSGrph USGrph RegGrph
21breqi 4399 . . 3 RegUSGrph USGrph RegGrph
3 oprabv 30298 . . 3 USGrph RegGrph
42, 3sylbi 195 . 2 RegUSGrph
5 isrusgra 30685 . . 3 RegUSGrph USGrph VDeg
6 isrgra 30684 . . . . . 6 RegGrph VDeg
76biimprcd 225 . . . . 5 VDeg RegGrph
873adant1 1006 . . . 4 USGrph VDeg RegGrph
98com12 31 . . 3 USGrph VDeg RegGrph
105, 9sylbid 215 . 2 RegUSGrph RegGrph
114, 10mpcom 36 1 RegUSGrph RegGrph
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 965   wceq 1370   wcel 1758  wral 2795  cvv 3071  cop 3984   class class class wbr 4393  cfv 5519  (class class class)co 6193  coprab 6194  cn0 10683   USGrph cusg 23409   VDeg cvdg 23708   RegGrph crgra 30680   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:  rusgra0edg  30714
 Copyright terms: Public domain W3C validator