Step |
Hyp |
Ref |
Expression |
1 |
|
0sno |
Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |- |
2 |
|
rightssold |
Could not format ( 0s e. No -> ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) ) : No typesetting found for |- ( 0s e. No -> ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) ) with typecode |- |
3 |
1 2
|
ax-mp |
Could not format ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) : No typesetting found for |- ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) with typecode |- |
4 |
|
bday0s |
Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |- |
5 |
4
|
fveq2i |
Could not format ( _Old ` ( bday ` 0s ) ) = ( _Old ` (/) ) : No typesetting found for |- ( _Old ` ( bday ` 0s ) ) = ( _Old ` (/) ) with typecode |- |
6 |
|
old0 |
|
7 |
5 6
|
eqtri |
Could not format ( _Old ` ( bday ` 0s ) ) = (/) : No typesetting found for |- ( _Old ` ( bday ` 0s ) ) = (/) with typecode |- |
8 |
|
sseq0 |
Could not format ( ( ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) /\ ( _Old ` ( bday ` 0s ) ) = (/) ) -> ( _R ` 0s ) = (/) ) : No typesetting found for |- ( ( ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) /\ ( _Old ` ( bday ` 0s ) ) = (/) ) -> ( _R ` 0s ) = (/) ) with typecode |- |
9 |
3 7 8
|
mp2an |
Could not format ( _R ` 0s ) = (/) : No typesetting found for |- ( _R ` 0s ) = (/) with typecode |- |