| Step |
Hyp |
Ref |
Expression |
| 1 |
|
f0 |
|- (/) : (/) --> (/) |
| 2 |
|
dm0 |
|- dom (/) = (/) |
| 3 |
|
pw0 |
|- ~P (/) = { (/) } |
| 4 |
3
|
difeq1i |
|- ( ~P (/) \ { (/) } ) = ( { (/) } \ { (/) } ) |
| 5 |
|
difid |
|- ( { (/) } \ { (/) } ) = (/) |
| 6 |
4 5
|
eqtri |
|- ( ~P (/) \ { (/) } ) = (/) |
| 7 |
2 6
|
feq23i |
|- ( (/) : dom (/) --> ( ~P (/) \ { (/) } ) <-> (/) : (/) --> (/) ) |
| 8 |
1 7
|
mpbir |
|- (/) : dom (/) --> ( ~P (/) \ { (/) } ) |
| 9 |
|
0ex |
|- (/) e. _V |
| 10 |
|
vtxval0 |
|- ( Vtx ` (/) ) = (/) |
| 11 |
10
|
eqcomi |
|- (/) = ( Vtx ` (/) ) |
| 12 |
|
iedgval0 |
|- ( iEdg ` (/) ) = (/) |
| 13 |
12
|
eqcomi |
|- (/) = ( iEdg ` (/) ) |
| 14 |
11 13
|
isuhgr |
|- ( (/) e. _V -> ( (/) e. UHGraph <-> (/) : dom (/) --> ( ~P (/) \ { (/) } ) ) ) |
| 15 |
9 14
|
ax-mp |
|- ( (/) e. UHGraph <-> (/) : dom (/) --> ( ~P (/) \ { (/) } ) ) |
| 16 |
8 15
|
mpbir |
|- (/) e. UHGraph |