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

Metamath Proof Explorer

Theorem elfvunirn

Description: A function value is a subset of the union of the range. (An artifact of our function value definition, compare elfvdm ). (Contributed by Thierry Arnoux, 13-Nov-2016) Remove functionhood antecedent. (Revised by SN, 10-Jan-2025)

Ref Expression
Assertion elfvunirn ⊢ B ∈ F ⁡ A → B ∈ ⋃ ran ⁡ F

Proof

Step Hyp Ref Expression
1 ne0i ⊢ B ∈ F ⁡ A → F ⁡ A ≠ ∅
2 fvn0fvelrn ⊢ F ⁡ A ≠ ∅ → F ⁡ A ∈ ran ⁡ F
3 elssuni ⊢ F ⁡ A ∈ ran ⁡ F → F ⁡ A ⊆ ⋃ ran ⁡ F
4 1 2 3 3syl ⊢ B ∈ F ⁡ A → F ⁡ A ⊆ ⋃ ran ⁡ F
5 4 sseld ⊢ B ∈ F ⁡ A → B ∈ F ⁡ A → B ∈ ⋃ ran ⁡ F
6 5 pm2.43i ⊢ B ∈ F ⁡ A → B ∈ ⋃ ran ⁡ F