Step |
Hyp |
Ref |
Expression |
1 |
|
imadif |
|- ( Fun `' F -> ( F " ( A \ ( A \ B ) ) ) = ( ( F " A ) \ ( F " ( A \ B ) ) ) ) |
2 |
|
imadif |
|- ( Fun `' F -> ( F " ( A \ B ) ) = ( ( F " A ) \ ( F " B ) ) ) |
3 |
2
|
difeq2d |
|- ( Fun `' F -> ( ( F " A ) \ ( F " ( A \ B ) ) ) = ( ( F " A ) \ ( ( F " A ) \ ( F " B ) ) ) ) |
4 |
1 3
|
eqtrd |
|- ( Fun `' F -> ( F " ( A \ ( A \ B ) ) ) = ( ( F " A ) \ ( ( F " A ) \ ( F " B ) ) ) ) |
5 |
|
dfin4 |
|- ( A i^i B ) = ( A \ ( A \ B ) ) |
6 |
5
|
imaeq2i |
|- ( F " ( A i^i B ) ) = ( F " ( A \ ( A \ B ) ) ) |
7 |
|
dfin4 |
|- ( ( F " A ) i^i ( F " B ) ) = ( ( F " A ) \ ( ( F " A ) \ ( F " B ) ) ) |
8 |
4 6 7
|
3eqtr4g |
|- ( Fun `' F -> ( F " ( A i^i B ) ) = ( ( F " A ) i^i ( F " B ) ) ) |