Metamath Proof Explorer

Theorem elunirn2

Description: Condition for the membership in the union of the range of a function. (Contributed by Thierry Arnoux, 13-Nov-2016)

Ref Expression
Assertion elunirn2 ⊢ Fun ⁡ F ∧ B ∈ F ⁡ A → B ∈ ⋃ ran ⁡ F

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ B ∈ F ⁡ A → A ∈ dom ⁡ F
2 fveq2 ⊢ x = A → F ⁡ x = F ⁡ A
3 2 eleq2d ⊢ x = A → B ∈ F ⁡ x ↔ B ∈ F ⁡ A
4 3 rspcev ⊢ A ∈ dom ⁡ F ∧ B ∈ F ⁡ A → ∃ x ∈ dom ⁡ F B ∈ F ⁡ x
5 1 4 mpancom ⊢ B ∈ F ⁡ A → ∃ x ∈ dom ⁡ F B ∈ F ⁡ x
6 5 adantl ⊢ Fun ⁡ F ∧ B ∈ F ⁡ A → ∃ x ∈ dom ⁡ F B ∈ F ⁡ x
7 elunirn ⊢ Fun ⁡ F → B ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F B ∈ F ⁡ x
8 7 adantr ⊢ Fun ⁡ F ∧ B ∈ F ⁡ A → B ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F B ∈ F ⁡ x
9 6 8 mpbird ⊢ Fun ⁡ F ∧ B ∈ F ⁡ A → B ∈ ⋃ ran ⁡ F