Theorem intpreima

Description: Preimage of an intersection. (Contributed by FL, 28-Apr-2012)

	Ref	Expression
Assertion	intpreima	⊢ ( ( Fun 𝐹 ∧ 𝐴 ≠ ∅ ) → ( ◡ 𝐹 “ ∩ 𝐴 ) = ∩ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		intiin	⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥
2	1	imaeq2i	⊢ ( ◡ 𝐹 “ ∩ 𝐴 ) = ( ◡ 𝐹 “ ∩ 𝑥 ∈ 𝐴 𝑥 )
3		iinpreima	⊢ ( ( Fun 𝐹 ∧ 𝐴 ≠ ∅ ) → ( ◡ 𝐹 “ ∩ 𝑥 ∈ 𝐴 𝑥 ) = ∩ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) )
4	2 3	eqtrid	⊢ ( ( Fun 𝐹 ∧ 𝐴 ≠ ∅ ) → ( ◡ 𝐹 “ ∩ 𝐴 ) = ∩ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) )