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

Theorem isrusgra 25331
 Description: The property of being a k-regular undirected simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
Assertion
Ref Expression
isrusgra RegUSGrph USGrph VDeg
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem isrusgra
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-br 4395 . . . . 5 RegUSGrph RegUSGrph
2 df-rusgra 25329 . . . . . 6 RegUSGrph USGrph RegGrph
32eleq2i 2480 . . . . 5 RegUSGrph USGrph RegGrph
41, 3bitri 249 . . . 4 RegUSGrph USGrph RegGrph
5 breq12 4399 . . . . . . 7 USGrph USGrph
653adant3 1017 . . . . . 6 USGrph USGrph
7 opeq12 4160 . . . . . . . 8
873adant3 1017 . . . . . . 7
9 simp3 999 . . . . . . 7
108, 9breq12d 4407 . . . . . 6 RegGrph RegGrph
116, 10anbi12d 709 . . . . 5 USGrph RegGrph USGrph RegGrph
1211eloprabga 6369 . . . 4 USGrph RegGrph USGrph RegGrph
134, 12syl5bb 257 . . 3 RegUSGrph USGrph RegGrph
14 isrgra 25330 . . . 4 RegGrph VDeg
1514anbi2d 702 . . 3 USGrph RegGrph USGrph VDeg
1613, 15bitrd 253 . 2 RegUSGrph USGrph VDeg
17 3anass 978 . 2 USGrph VDeg USGrph VDeg
1816, 17syl6bbr 263 1 RegUSGrph USGrph VDeg
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 367   w3a 974   wceq 1405   wcel 1842  wral 2753  cop 3977   class class class wbr 4394  cfv 5568  (class class class)co 6277  coprab 6278  cn0 10835   USGrph cusg 24734   VDeg cvdg 25297   RegGrph crgra 25326   RegUSGrph crusgra 25327 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-iota 5532  df-fv 5576  df-ov 6280  df-oprab 6281  df-rgra 25328  df-rusgra 25329 This theorem is referenced by:  rusgraprop  25333  rusgrargra  25334  isrusgusrg  25336  cusgraisrusgra  25342  frgraregorufrg  25476
 Copyright terms: Public domain W3C validator