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

Theorem clwlknclwlkdifs 25686
 Description: The set of walks of length n starting with a fixed vertex and ending not at this vertex is the difference between the set of walks of length n starting with this vertex and the set of walks of length n starting with this vertex and ending at this vertex. (Contributed by Alexander van der Vekens, 30-Sep-2018.)
Hypotheses
Ref Expression
clwlknclwlkdif.a WWalksN lastS
clwlknclwlkdif.b WWalksN lastS
Assertion
Ref Expression
clwlknclwlkdifs WWalksN

Proof of Theorem clwlknclwlkdifs
StepHypRef Expression
1 clwlknclwlkdif.a . 2 WWalksN lastS
2 clwlknclwlkdif.b . . . 4 WWalksN lastS
32difeq2i 3580 . . 3 WWalksN WWalksN WWalksN lastS
4 difrab 3747 . . 3 WWalksN WWalksN lastS WWalksN lastS
5 ianor 490 . . . . . . . 8 lastS lastS
6 eqeq2 2437 . . . . . . . . . . . 12 lastS lastS
76notbid 295 . . . . . . . . . . 11 lastS lastS
8 df-ne 2616 . . . . . . . . . . . . . 14 lastS lastS
98biimpri 209 . . . . . . . . . . . . 13 lastS lastS
109anim2i 571 . . . . . . . . . . . 12 lastS lastS
1110ex 435 . . . . . . . . . . 11 lastS lastS
127, 11sylbid 218 . . . . . . . . . 10 lastS lastS
1312com12 32 . . . . . . . . 9 lastS lastS
14 pm2.21 111 . . . . . . . . 9 lastS
1513, 14jaoi 380 . . . . . . . 8 lastS lastS
165, 15sylbi 198 . . . . . . 7 lastS lastS
1716impcom 431 . . . . . 6 lastS lastS
18 simpl 458 . . . . . . 7 lastS
19 neeq2 2703 . . . . . . . . . . 11 lastS lastS
2019eqcoms 2434 . . . . . . . . . 10 lastS lastS
21 df-ne 2616 . . . . . . . . . . 11 lastS lastS
2221biimpi 197 . . . . . . . . . 10 lastS lastS
2320, 22syl6bi 231 . . . . . . . . 9 lastS lastS
2423imp 430 . . . . . . . 8 lastS lastS
2524intnanrd 925 . . . . . . 7 lastS lastS
2618, 25jca 534 . . . . . 6 lastS lastS
2717, 26impbii 190 . . . . 5 lastS lastS
2827a1i 11 . . . 4 WWalksN lastS lastS
2928rabbiia 3068 . . 3 WWalksN lastS WWalksN lastS
303, 4, 293eqtrri 2456 . 2 WWalksN lastS WWalksN
311, 30eqtri 2451 1 WWalksN
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wo 369   wa 370   wceq 1437   wcel 1872   wne 2614  crab 2775   cdif 3433  cfv 5601  (class class class)co 6305  cc0 9546   lastS clsw 12661   WWalksN cwwlkn 25404 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rab 2780  df-v 3082  df-dif 3439 This theorem is referenced by:  clwlknclwlkdifnum  25687
 Copyright terms: Public domain W3C validator