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

Theorem numclwwlkdisj 25794
 Description: The sets of closed walks starting at different vertices in an undirected simple graph are disjunct. (Contributed by Alexander van der Vekens, 7-Oct-2018.)
Hypothesis
Ref Expression
numclwwlk.c ClWWalksN
Assertion
Ref Expression
numclwwlkdisj Disj
Distinct variable groups:   ,   ,   ,   ,,   ,   ,,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem numclwwlkdisj
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 inrab 3745 . . . . 5
2 eqtr2 2449 . . . . . . . 8
32con3i 140 . . . . . . 7
43ralrimivw 2840 . . . . . 6
5 rabeq0 3784 . . . . . 6
64, 5sylibr 215 . . . . 5
71, 6syl5eq 2475 . . . 4
87orri 377 . . 3
98rgen2w 2787 . 2
10 eqeq2 2437 . . . 4
1110rabbidv 3072 . . 3
1211disjor 4405 . 2 Disj
139, 12mpbir 212 1 Disj
 Colors of variables: wff setvar class Syntax hints:   wn 3   wo 369   wa 370   wceq 1437  wral 2775  crab 2779   cin 3435  c0 3761  Disj wdisj 4391   cmpt 4479  cfv 5598  (class class class)co 6302  cc0 9540  cn0 10870   ClWWalksN cclwwlkn 25463 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rmo 2783  df-rab 2784  df-v 3083  df-dif 3439  df-in 3443  df-nul 3762  df-disj 4392 This theorem is referenced by:  numclwwlk4  25824
 Copyright terms: Public domain W3C validator