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

Step	Hyp	Ref	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 𝑤
7	6	cv 1652	. . . . . 6 class 𝑤
8		chash 13370	. . . . . 6 class ♯
9	7, 8	cfv 6101	. . . . 5 class (♯‘𝑤)
10	2	cv 1652	. . . . 5 class 𝑛
11	9, 10	wceq 1653	. . . 4 wff (♯‘𝑤) = 𝑛
12	3	cv 1652	. . . . 5 class 𝑔
13		cclwwlk 27274	. . . . 5 class ClWWalks
14	12, 13	cfv 6101	. . . 4 class (ClWWalks‘𝑔)
15	11, 6, 14	crab 3093	. . 3 class {𝑤 ∈ (ClWWalks‘𝑔) ∣ (♯‘𝑤) = 𝑛}
16	2, 3, 4, 5, 15	cmpt2 6880	. 2 class (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalks‘𝑔) ∣ (♯‘𝑤) = 𝑛})
17	1, 16	wceq 1653	1 wff ClWWalksNOLD = (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalks‘𝑔) ∣ (♯‘𝑤) = 𝑛})

This definition is referenced by:  clwwlknOLD  27331