| Step |
Hyp |
Ref |
Expression |
| 1 |
|
stgredg |
Could not format ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : No typesetting found for |- ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) with typecode |- |
| 2 |
1
|
eleq2d |
Could not format ( N e. NN0 -> ( E e. ( Edg ` ( StarGr ` N ) ) <-> E e. { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) : No typesetting found for |- ( N e. NN0 -> ( E e. ( Edg ` ( StarGr ` N ) ) <-> E e. { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) with typecode |- |
| 3 |
|
eqeq1 |
|
| 4 |
3
|
rexbidv |
|
| 5 |
4
|
elrab |
|
| 6 |
|
prex |
|
| 7 |
|
eleq1 |
|
| 8 |
6 7
|
mpbiri |
|
| 9 |
|
elpwg |
|
| 10 |
8 9
|
syl |
|
| 11 |
10
|
a1i |
|
| 12 |
11
|
rexlimiv |
|
| 13 |
5 12
|
bianim |
|
| 14 |
2 13
|
bitrdi |
Could not format ( N e. NN0 -> ( E e. ( Edg ` ( StarGr ` N ) ) <-> ( E C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) E = { 0 , x } ) ) ) : No typesetting found for |- ( N e. NN0 -> ( E e. ( Edg ` ( StarGr ` N ) ) <-> ( E C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) E = { 0 , x } ) ) ) with typecode |- |