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 bitr2id
 |-  ( 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 } ) ) )