| Step |
Hyp |
Ref |
Expression |
| 1 |
|
negsf |
Could not format -us : No --> No : No typesetting found for |- -us : No --> No with typecode |- |
| 2 |
|
negscl |
Could not format ( x e. No -> ( -us ` x ) e. No ) : No typesetting found for |- ( x e. No -> ( -us ` x ) e. No ) with typecode |- |
| 3 |
|
negnegs |
Could not format ( x e. No -> ( -us ` ( -us ` x ) ) = x ) : No typesetting found for |- ( x e. No -> ( -us ` ( -us ` x ) ) = x ) with typecode |- |
| 4 |
3
|
eqcomd |
Could not format ( x e. No -> x = ( -us ` ( -us ` x ) ) ) : No typesetting found for |- ( x e. No -> x = ( -us ` ( -us ` x ) ) ) with typecode |- |
| 5 |
|
fveq2 |
Could not format ( y = ( -us ` x ) -> ( -us ` y ) = ( -us ` ( -us ` x ) ) ) : No typesetting found for |- ( y = ( -us ` x ) -> ( -us ` y ) = ( -us ` ( -us ` x ) ) ) with typecode |- |
| 6 |
5
|
eqeq2d |
Could not format ( y = ( -us ` x ) -> ( x = ( -us ` y ) <-> x = ( -us ` ( -us ` x ) ) ) ) : No typesetting found for |- ( y = ( -us ` x ) -> ( x = ( -us ` y ) <-> x = ( -us ` ( -us ` x ) ) ) ) with typecode |- |
| 7 |
6
|
rspcev |
Could not format ( ( ( -us ` x ) e. No /\ x = ( -us ` ( -us ` x ) ) ) -> E. y e. No x = ( -us ` y ) ) : No typesetting found for |- ( ( ( -us ` x ) e. No /\ x = ( -us ` ( -us ` x ) ) ) -> E. y e. No x = ( -us ` y ) ) with typecode |- |
| 8 |
2 4 7
|
syl2anc |
Could not format ( x e. No -> E. y e. No x = ( -us ` y ) ) : No typesetting found for |- ( x e. No -> E. y e. No x = ( -us ` y ) ) with typecode |- |
| 9 |
8
|
rgen |
Could not format A. x e. No E. y e. No x = ( -us ` y ) : No typesetting found for |- A. x e. No E. y e. No x = ( -us ` y ) with typecode |- |
| 10 |
|
dffo3 |
Could not format ( -us : No -onto-> No <-> ( -us : No --> No /\ A. x e. No E. y e. No x = ( -us ` y ) ) ) : No typesetting found for |- ( -us : No -onto-> No <-> ( -us : No --> No /\ A. x e. No E. y e. No x = ( -us ` y ) ) ) with typecode |- |
| 11 |
1 9 10
|
mpbir2an |
Could not format -us : No -onto-> No : No typesetting found for |- -us : No -onto-> No with typecode |- |