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

Metamath Proof Explorer

Theorem intpreima

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

Ref Expression
Assertion intpreima ⊢ Fun ⁡ F ∧ A ≠ ∅ → F -1 ⋂ A = ⋂ x ∈ A F -1 x

Proof

Step Hyp Ref Expression
1 intiin ⊢ ⋂ A = ⋂ x ∈ A x
2 1 imaeq2i ⊢ F -1 ⋂ A = F -1 ⋂ x ∈ A x
3 iinpreima ⊢ Fun ⁡ F ∧ A ≠ ∅ → F -1 ⋂ x ∈ A x = ⋂ x ∈ A F -1 x
4 2 3 eqtrid ⊢ Fun ⁡ F ∧ A ≠ ∅ → F -1 ⋂ A = ⋂ x ∈ A F -1 x