Metamath Proof Explorer


Theorem imain

Description: The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009)

Ref Expression
Assertion imain
|- ( Fun `' F -> ( F " ( A i^i B ) ) = ( ( F " A ) i^i ( F " B ) ) )

Proof

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 ) ) )