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 ) C_ U. ran F

Proof

Step Hyp Ref Expression
1 df-ov 
 |-  ( X F Y ) = ( F ` <. X , Y >. )
2 fvssunirn 
 |-  ( F ` <. X , Y >. ) C_ U. ran F
3 1 2 eqsstri 
 |-  ( X F Y ) C_ U. ran F