Step |
Hyp |
Ref |
Expression |
1 |
|
naryfval.i |
|
2 |
1
|
naryfval |
Could not format ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) : No typesetting found for |- ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) with typecode |- |
3 |
2
|
eleq2d |
Could not format ( N e. NN0 -> ( F e. ( N -aryF X ) <-> F e. ( X ^m ( X ^m I ) ) ) ) : No typesetting found for |- ( N e. NN0 -> ( F e. ( N -aryF X ) <-> F e. ( X ^m ( X ^m I ) ) ) ) with typecode |- |
4 |
|
ovex |
|
5 |
|
elmapg |
|
6 |
4 5
|
mpan2 |
|
7 |
3 6
|
sylan9bb |
Could not format ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : ( X ^m I ) --> X ) ) : No typesetting found for |- ( ( N e. NN0 /\ X e. V ) -> ( F e. ( N -aryF X ) <-> F : ( X ^m I ) --> X ) ) with typecode |- |