Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1047.1 |
|
2 |
|
bnj1047.2 |
Could not format ( et' <-> [. j / i ]. et ) : No typesetting found for |- ( et' <-> [. j / i ]. et ) with typecode |- |
3 |
2
|
imbi2i |
Could not format ( ( j _E i -> et' ) <-> ( j _E i -> [. j / i ]. et ) ) : No typesetting found for |- ( ( j _E i -> et' ) <-> ( j _E i -> [. j / i ]. et ) ) with typecode |- |
4 |
3
|
ralbii |
Could not format ( A. j e. n ( j _E i -> et' ) <-> A. j e. n ( j _E i -> [. j / i ]. et ) ) : No typesetting found for |- ( A. j e. n ( j _E i -> et' ) <-> A. j e. n ( j _E i -> [. j / i ]. et ) ) with typecode |- |
5 |
1 4
|
bitr4i |
Could not format ( rh <-> A. j e. n ( j _E i -> et' ) ) : No typesetting found for |- ( rh <-> A. j e. n ( j _E i -> et' ) ) with typecode |- |