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