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

Metamath Proof Explorer

Theorem eluniima

Description: Membership in the union of an image of a function. (Contributed by NM, 28-Sep-2006)

Ref Expression
Assertion eluniima ⊢ Fun ⁡ F → B ∈ ⋃ F A ↔ ∃ x ∈ A B ∈ F ⁡ x

Proof

Step Hyp Ref Expression
1 funiunfv ⊢ Fun ⁡ F → ⋃ x ∈ A F ⁡ x = ⋃ F A
2 1 eleq2d ⊢ Fun ⁡ F → B ∈ ⋃ x ∈ A F ⁡ x ↔ B ∈ ⋃ F A
3 eliun ⊢ B ∈ ⋃ x ∈ A F ⁡ x ↔ ∃ x ∈ A B ∈ F ⁡ x
4 2 3 bitr3di ⊢ Fun ⁡ F → B ∈ ⋃ F A ↔ ∃ x ∈ A B ∈ F ⁡ x