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 ∩ B C = A C ∩ B C

Proof

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