Metamath Proof Explorer

Theorem inpreima

Description: Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Jun-2016)

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

Proof

Step Hyp Ref Expression
1 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
2 imain 
 |-  ( Fun `' `' F -> ( `' F " ( A i^i B ) ) = ( ( `' F " A ) i^i ( `' F " B ) ) )
3 1 2 syl 
 |-  ( Fun F -> ( `' F " ( A i^i B ) ) = ( ( `' F " A ) i^i ( `' F " B ) ) )