Step |
Hyp |
Ref |
Expression |
1 |
|
wwlksn |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) |
2 |
1
|
eleq2d |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ 𝑊 ∈ { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ) ) |
3 |
|
fveqeq2 |
⊢ ( 𝑤 = 𝑊 → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) |
4 |
3
|
elrab |
⊢ ( 𝑊 ∈ { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) |
5 |
2 4
|
bitrdi |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ) |