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∈V→A∩BC=AC∩BC

Proof

Step Hyp Ref Expression
1 elin ⊢x∈AC∩BC↔x∈AC∧x∈BC
2 elin ⊢Cx∈A∩B↔Cx∈A∧Cx∈B
3 2 a1i ⊢C∈V→Cx∈A∩B↔Cx∈A∧Cx∈B
4 elimasng ⊢C∈V∧x∈V→x∈A∩BC↔Cx∈A∩B
5 4 elvd ⊢C∈V→x∈A∩BC↔Cx∈A∩B
6 elimasng ⊢C∈V∧x∈V→x∈AC↔Cx∈A
7 6 elvd ⊢C∈V→x∈AC↔Cx∈A
8 elimasng ⊢C∈V∧x∈V→x∈BC↔Cx∈B
9 8 elvd ⊢C∈V→x∈BC↔Cx∈B
10 7 9 anbi12d ⊢C∈V→x∈AC∧x∈BC↔Cx∈A∧Cx∈B
11 3 5 10 3bitr4rd ⊢C∈V→x∈AC∧x∈BC↔x∈A∩BC
12 1 11 bitr2id ⊢C∈V→x∈A∩BC↔x∈AC∩BC
13 12 eqrdv ⊢C∈V→A∩BC=AC∩BC