Metamath Proof Explorer

Theorem fnunirn

Description: Membership in a union of some function-defined family of sets. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion fnunirn ⊢ F Fn I → A ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ I A ∈ F ⁡ x

Proof

Step Hyp Ref Expression
1 fnfun ⊢ F Fn I → Fun ⁡ F
2 elunirn ⊢ Fun ⁡ F → A ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F A ∈ F ⁡ x
3 1 2 syl ⊢ F Fn I → A ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F A ∈ F ⁡ x
4 fndm ⊢ F Fn I → dom ⁡ F = I
5 4 rexeqdv ⊢ F Fn I → ∃ x ∈ dom ⁡ F A ∈ F ⁡ x ↔ ∃ x ∈ I A ∈ F ⁡ x
6 3 5 bitrd ⊢ F Fn I → A ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ I A ∈ F ⁡ x