Step |
Hyp |
Ref |
Expression |
1 |
|
df-new |
Could not format _New = ( x e. On |-> ( ( _Made ` x ) \ ( _Old ` x ) ) ) : No typesetting found for |- _New = ( x e. On |-> ( ( _Made ` x ) \ ( _Old ` x ) ) ) with typecode |- |
2 |
|
madef |
Could not format _Made : On --> ~P No : No typesetting found for |- _Made : On --> ~P No with typecode |- |
3 |
2
|
ffvelcdmi |
Could not format ( x e. On -> ( _Made ` x ) e. ~P No ) : No typesetting found for |- ( x e. On -> ( _Made ` x ) e. ~P No ) with typecode |- |
4 |
3
|
elpwid |
Could not format ( x e. On -> ( _Made ` x ) C_ No ) : No typesetting found for |- ( x e. On -> ( _Made ` x ) C_ No ) with typecode |- |
5 |
4
|
ssdifssd |
Could not format ( x e. On -> ( ( _Made ` x ) \ ( _Old ` x ) ) C_ No ) : No typesetting found for |- ( x e. On -> ( ( _Made ` x ) \ ( _Old ` x ) ) C_ No ) with typecode |- |
6 |
|
fvex |
Could not format ( _Made ` x ) e. _V : No typesetting found for |- ( _Made ` x ) e. _V with typecode |- |
7 |
6
|
difexi |
Could not format ( ( _Made ` x ) \ ( _Old ` x ) ) e. _V : No typesetting found for |- ( ( _Made ` x ) \ ( _Old ` x ) ) e. _V with typecode |- |
8 |
7
|
elpw |
Could not format ( ( ( _Made ` x ) \ ( _Old ` x ) ) e. ~P No <-> ( ( _Made ` x ) \ ( _Old ` x ) ) C_ No ) : No typesetting found for |- ( ( ( _Made ` x ) \ ( _Old ` x ) ) e. ~P No <-> ( ( _Made ` x ) \ ( _Old ` x ) ) C_ No ) with typecode |- |
9 |
5 8
|
sylibr |
Could not format ( x e. On -> ( ( _Made ` x ) \ ( _Old ` x ) ) e. ~P No ) : No typesetting found for |- ( x e. On -> ( ( _Made ` x ) \ ( _Old ` x ) ) e. ~P No ) with typecode |- |
10 |
1 9
|
fmpti |
Could not format _New : On --> ~P No : No typesetting found for |- _New : On --> ~P No with typecode |- |