Step |
Hyp |
Ref |
Expression |
1 |
|
bj-diagval2 |
Could not format ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) ) : No typesetting found for |- ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) ) with typecode |- |
2 |
1
|
eleq2d |
Could not format ( A e. V -> ( B e. ( _Id ` A ) <-> B e. ( _I i^i ( A X. A ) ) ) ) : No typesetting found for |- ( A e. V -> ( B e. ( _Id ` A ) <-> B e. ( _I i^i ( A X. A ) ) ) ) with typecode |- |
3 |
|
elin |
|
4 |
|
ancom |
|
5 |
|
bj-elid4 |
|
6 |
5
|
pm5.32i |
|
7 |
3 4 6
|
3bitri |
|
8 |
2 7
|
syl6bb |
Could not format ( A e. V -> ( B e. ( _Id ` A ) <-> ( B e. ( A X. A ) /\ ( 1st ` B ) = ( 2nd ` B ) ) ) ) : No typesetting found for |- ( A e. V -> ( B e. ( _Id ` A ) <-> ( B e. ( A X. A ) /\ ( 1st ` B ) = ( 2nd ` B ) ) ) ) with typecode |- |