Step |
Hyp |
Ref |
Expression |
1 |
|
bnj591.1 |
Could not format ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |- |
2 |
1
|
sbcbii |
Could not format ( [. k / j ]. th <-> [. k / j ]. ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( [. k / j ]. th <-> [. k / j ]. ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |- |
3 |
|
vex |
|
4 |
|
fveq2 |
|
5 |
|
fveq2 |
|
6 |
4 5
|
eqeq12d |
|
7 |
6
|
imbi2d |
Could not format ( j = k -> ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) ) : No typesetting found for |- ( j = k -> ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) ) with typecode |- |
8 |
3 7
|
sbcie |
Could not format ( [. k / j ]. ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) : No typesetting found for |- ( [. k / j ]. ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) with typecode |- |
9 |
2 8
|
bitri |
Could not format ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) : No typesetting found for |- ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) with typecode |- |