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	⊢ ( 𝐶 ∈ 𝑉 → ( ( 𝐴 ∩ 𝐵 ) “ { 𝐶 } ) = ( ( 𝐴 “ { 𝐶 } ) ∩ ( 𝐵 “ { 𝐶 } ) ) )