MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-clwwlknOLD Structured version   Visualization version   GIF version

Definition df-clwwlknOLD 27329
Description: Obsolete version of df-clwwlkn 27328 as of 22-Mar-2022. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (New usage is discouraged.)
Assertion
Ref Expression
df-clwwlknOLD ClWWalksNOLD = (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalks‘𝑔) ∣ (♯‘𝑤) = 𝑛})
Distinct variable group:   𝑔,𝑛,𝑤

Detailed syntax breakdown of Definition df-clwwlknOLD
StepHypRef Expression
1 cclwwlknold 27327 . 2 class ClWWalksNOLD
2 vn . . 3 setvar 𝑛
3 vg . . 3 setvar 𝑔
4 cn 11312 . . 3 class
5 cvv 3385 . . 3 class V
6 vw . . . . . . 7 setvar 𝑤
76cv 1652 . . . . . 6 class 𝑤
8 chash 13370 . . . . . 6 class
97, 8cfv 6101 . . . . 5 class (♯‘𝑤)
102cv 1652 . . . . 5 class 𝑛
119, 10wceq 1653 . . . 4 wff (♯‘𝑤) = 𝑛
123cv 1652 . . . . 5 class 𝑔
13 cclwwlk 27274 . . . . 5 class ClWWalks
1412, 13cfv 6101 . . . 4 class (ClWWalks‘𝑔)
1511, 6, 14crab 3093 . . 3 class {𝑤 ∈ (ClWWalks‘𝑔) ∣ (♯‘𝑤) = 𝑛}
162, 3, 4, 5, 15cmpt2 6880 . 2 class (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalks‘𝑔) ∣ (♯‘𝑤) = 𝑛})
171, 16wceq 1653 1 wff ClWWalksNOLD = (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalks‘𝑔) ∣ (♯‘𝑤) = 𝑛})
Colors of variables: wff setvar class
This definition is referenced by:  clwwlknOLD  27331
  Copyright terms: Public domain W3C validator