Step |
Hyp |
Ref |
Expression |
1 |
|
fveq1 |
|- ( w = W -> ( w ` 0 ) = ( W ` 0 ) ) |
2 |
1
|
eqeq1d |
|- ( w = W -> ( ( w ` 0 ) = A <-> ( W ` 0 ) = A ) ) |
3 |
|
fveq1 |
|- ( w = W -> ( w ` N ) = ( W ` N ) ) |
4 |
3
|
eqeq1d |
|- ( w = W -> ( ( w ` N ) = B <-> ( W ` N ) = B ) ) |
5 |
2 4
|
anbi12d |
|- ( w = W -> ( ( ( w ` 0 ) = A /\ ( w ` N ) = B ) <-> ( ( W ` 0 ) = A /\ ( W ` N ) = B ) ) ) |
6 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
7 |
6
|
iswwlksnon |
|- ( A ( N WWalksNOn G ) B ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } |
8 |
5 7
|
elrab2 |
|- ( W e. ( A ( N WWalksNOn G ) B ) <-> ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = A /\ ( W ` N ) = B ) ) ) |
9 |
|
3anass |
|- ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = A /\ ( W ` N ) = B ) <-> ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = A /\ ( W ` N ) = B ) ) ) |
10 |
8 9
|
bitr4i |
|- ( W e. ( A ( N WWalksNOn G ) B ) <-> ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = A /\ ( W ` N ) = B ) ) |