Step |
Hyp |
Ref |
Expression |
1 |
|
fveqeq2 |
|- ( y = x -> ( ( # ` y ) = 2 <-> ( # ` x ) = 2 ) ) |
2 |
1
|
cbvrabv |
|- { y e. ~P V | ( # ` y ) = 2 } = { x e. ~P V | ( # ` x ) = 2 } |
3 |
2
|
cusgrexilem1 |
|- ( V e. W -> ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) e. _V ) |
4 |
2
|
cusgrexi |
|- ( V e. W -> <. V , ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) >. e. ComplUSGraph ) |
5 |
|
opeq2 |
|- ( e = ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) -> <. V , e >. = <. V , ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) >. ) |
6 |
5
|
eleq1d |
|- ( e = ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) -> ( <. V , e >. e. ComplUSGraph <-> <. V , ( _I |` { y e. ~P V | ( # ` y ) = 2 } ) >. e. ComplUSGraph ) ) |
7 |
3 4 6
|
spcedv |
|- ( V e. W -> E. e <. V , e >. e. ComplUSGraph ) |