Step |
Hyp |
Ref |
Expression |
1 |
|
rightssold |
Could not format ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) : No typesetting found for |- ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) with typecode |- |
2 |
|
bday0s |
Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |- |
3 |
2
|
fveq2i |
Could not format ( _Old ` ( bday ` 0s ) ) = ( _Old ` (/) ) : No typesetting found for |- ( _Old ` ( bday ` 0s ) ) = ( _Old ` (/) ) with typecode |- |
4 |
|
old0 |
|
5 |
3 4
|
eqtri |
Could not format ( _Old ` ( bday ` 0s ) ) = (/) : No typesetting found for |- ( _Old ` ( bday ` 0s ) ) = (/) with typecode |- |
6 |
|
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 |- |
7 |
1 5 6
|
mp2an |
Could not format ( _R ` 0s ) = (/) : No typesetting found for |- ( _R ` 0s ) = (/) with typecode |- |