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