Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Vtx ` <. V , E >. ) = ( Vtx ` <. V , E >. ) |
2 |
1
|
isfusgr |
|- ( <. V , E >. e. FinUSGraph <-> ( <. V , E >. e. USGraph /\ ( Vtx ` <. V , E >. ) e. Fin ) ) |
3 |
|
opvtxfv |
|- ( ( V e. X /\ E e. Y ) -> ( Vtx ` <. V , E >. ) = V ) |
4 |
3
|
eleq1d |
|- ( ( V e. X /\ E e. Y ) -> ( ( Vtx ` <. V , E >. ) e. Fin <-> V e. Fin ) ) |
5 |
4
|
anbi2d |
|- ( ( V e. X /\ E e. Y ) -> ( ( <. V , E >. e. USGraph /\ ( Vtx ` <. V , E >. ) e. Fin ) <-> ( <. V , E >. e. USGraph /\ V e. Fin ) ) ) |
6 |
2 5
|
syl5bb |
|- ( ( V e. X /\ E e. Y ) -> ( <. V , E >. e. FinUSGraph <-> ( <. V , E >. e. USGraph /\ V e. Fin ) ) ) |