Metamath Proof Explorer

Theorem inimasn

Description: The intersection of the image of singleton. (Contributed by Thierry Arnoux, 16-Dec-2017)

Ref Expression
Assertion inimasn 
|- ( C e. V -> ( ( A i^i B ) " { C } ) = ( ( A " { C } ) i^i ( B " { C } ) ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( x e. ( ( A " { C } ) i^i ( B " { C } ) ) <-> ( x e. ( A " { C } ) /\ x e. ( B " { C } ) ) )
2 elin 
 |-  ( <. C , x >. e. ( A i^i B ) <-> ( <. C , x >. e. A /\ <. C , x >. e. B ) )
3 2 a1i 
 |-  ( C e. V -> ( <. C , x >. e. ( A i^i B ) <-> ( <. C , x >. e. A /\ <. C , x >. e. B ) ) )
4 elimasng 
 |-  ( ( C e. V /\ x e. _V ) -> ( x e. ( ( A i^i B ) " { C } ) <-> <. C , x >. e. ( A i^i B ) ) )
5 4 elvd 
 |-  ( C e. V -> ( x e. ( ( A i^i B ) " { C } ) <-> <. C , x >. e. ( A i^i B ) ) )
6 elimasng 
 |-  ( ( C e. V /\ x e. _V ) -> ( x e. ( A " { C } ) <-> <. C , x >. e. A ) )
7 6 elvd 
 |-  ( C e. V -> ( x e. ( A " { C } ) <-> <. C , x >. e. A ) )
8 elimasng 
 |-  ( ( C e. V /\ x e. _V ) -> ( x e. ( B " { C } ) <-> <. C , x >. e. B ) )
9 8 elvd 
 |-  ( C e. V -> ( x e. ( B " { C } ) <-> <. C , x >. e. B ) )
10 7 9 anbi12d 
 |-  ( C e. V -> ( ( x e. ( A " { C } ) /\ x e. ( B " { C } ) ) <-> ( <. C , x >. e. A /\ <. C , x >. e. B ) ) )
11 3 5 10 3bitr4rd 
 |-  ( C e. V -> ( ( x e. ( A " { C } ) /\ x e. ( B " { C } ) ) <-> x e. ( ( A i^i B ) " { C } ) ) )
12 1 11 syl5rbb 
 |-  ( C e. V -> ( x e. ( ( A i^i B ) " { C } ) <-> x e. ( ( A " { C } ) i^i ( B " { C } ) ) ) )
13 12 eqrdv 
 |-  ( C e. V -> ( ( A i^i B ) " { C } ) = ( ( A " { C } ) i^i ( B " { C } ) ) )