Metamath Proof Explorer

Theorem ovssunirn

Description: The result of an operation value is always a subset of the union of the range. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Assertion ovssunirn X F Y ran F


Step Hyp Ref Expression
1 df-ov X F Y = F X Y
2 fvssunirn F X Y ran F
3 1 2 eqsstri X F Y ran F