Step |
Hyp |
Ref |
Expression |
1 |
|
f10 |
|- (/) : (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } |
2 |
|
dm0 |
|- dom (/) = (/) |
3 |
|
f1eq2 |
|- ( dom (/) = (/) -> ( (/) : dom (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } <-> (/) : (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } ) ) |
4 |
2 3
|
ax-mp |
|- ( (/) : dom (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } <-> (/) : (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } ) |
5 |
1 4
|
mpbir |
|- (/) : dom (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } |
6 |
|
0ex |
|- (/) e. _V |
7 |
|
vtxval0 |
|- ( Vtx ` (/) ) = (/) |
8 |
7
|
eqcomi |
|- (/) = ( Vtx ` (/) ) |
9 |
|
iedgval0 |
|- ( iEdg ` (/) ) = (/) |
10 |
9
|
eqcomi |
|- (/) = ( iEdg ` (/) ) |
11 |
8 10
|
isusgr |
|- ( (/) e. _V -> ( (/) e. USGraph <-> (/) : dom (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } ) ) |
12 |
6 11
|
ax-mp |
|- ( (/) e. USGraph <-> (/) : dom (/) -1-1-> { x e. ( ~P (/) \ { (/) } ) | ( # ` x ) = 2 } ) |
13 |
5 12
|
mpbir |
|- (/) e. USGraph |