This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inimasn

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

Ref Expression
Assertion inimasn ( 𝐶 ∈ 𝑉 → ( ( 𝐴 ∩ 𝐵 ) “ { 𝐶 } ) = ( ( 𝐴 “ { 𝐶 } ) ∩ ( 𝐵 “ { 𝐶 } ) ) )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑥 ∈ ( ( 𝐴 “ { 𝐶 } ) ∩ ( 𝐵 “ { 𝐶 } ) ) ↔ ( 𝑥 ∈ ( 𝐴 “ { 𝐶 } ) ∧ 𝑥 ∈ ( 𝐵 “ { 𝐶 } ) ) )
2 elin ⊢ ( ⟨ 𝐶 , 𝑥 ⟩ ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( ⟨ 𝐶 , 𝑥 ⟩ ∈ 𝐴 ∧ ⟨ 𝐶 , 𝑥 ⟩ ∈ 𝐵 ) )
3 2 a1i ⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐶 , 𝑥 ⟩ ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( ⟨ 𝐶 , 𝑥 ⟩ ∈ 𝐴 ∧ ⟨ 𝐶 , 𝑥 ⟩ ∈ 𝐵 ) ) )
4 elimasng ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) “ { 𝐶 } ) ↔ ⟨ 𝐶 , 𝑥 ⟩ ∈ ( 𝐴 ∩ 𝐵 ) ) )
5 4 elvd ⊢ ( 𝐶 ∈ 𝑉 → ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) “ { 𝐶 } ) ↔ ⟨ 𝐶 , 𝑥 ⟩ ∈ ( 𝐴 ∩ 𝐵 ) ) )
6 elimasng ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( 𝐴 “ { 𝐶 } ) ↔ ⟨ 𝐶 , 𝑥 ⟩ ∈ 𝐴 ) )
7 6 elvd ⊢ ( 𝐶 ∈ 𝑉 → ( 𝑥 ∈ ( 𝐴 “ { 𝐶 } ) ↔ ⟨ 𝐶 , 𝑥 ⟩ ∈ 𝐴 ) )
8 elimasng ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( 𝐵 “ { 𝐶 } ) ↔ ⟨ 𝐶 , 𝑥 ⟩ ∈ 𝐵 ) )
9 8 elvd ⊢ ( 𝐶 ∈ 𝑉 → ( 𝑥 ∈ ( 𝐵 “ { 𝐶 } ) ↔ ⟨ 𝐶 , 𝑥 ⟩ ∈ 𝐵 ) )
10 7 9 anbi12d ⊢ ( 𝐶 ∈ 𝑉 → ( ( 𝑥 ∈ ( 𝐴 “ { 𝐶 } ) ∧ 𝑥 ∈ ( 𝐵 “ { 𝐶 } ) ) ↔ ( ⟨ 𝐶 , 𝑥 ⟩ ∈ 𝐴 ∧ ⟨ 𝐶 , 𝑥 ⟩ ∈ 𝐵 ) ) )
11 3 5 10 3bitr4rd ⊢ ( 𝐶 ∈ 𝑉 → ( ( 𝑥 ∈ ( 𝐴 “ { 𝐶 } ) ∧ 𝑥 ∈ ( 𝐵 “ { 𝐶 } ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) “ { 𝐶 } ) ) )
12 1 11 bitr2id ⊢ ( 𝐶 ∈ 𝑉 → ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) “ { 𝐶 } ) ↔ 𝑥 ∈ ( ( 𝐴 “ { 𝐶 } ) ∩ ( 𝐵 “ { 𝐶 } ) ) ) )
13 12 eqrdv ⊢ ( 𝐶 ∈ 𝑉 → ( ( 𝐴 ∩ 𝐵 ) “ { 𝐶 } ) = ( ( 𝐴 “ { 𝐶 } ) ∩ ( 𝐵 “ { 𝐶 } ) ) )