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

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 \subseteq ⋃ ran F$

Step	Hyp	Ref	Expression
1		df-ov	$⊢ X F Y = F (⟨X, Y⟩)$
2		fvssunirn	$⊢ F (⟨X, Y⟩) \subseteq ⋃ ran F$
3	1 2	eqsstri	$⊢ X F Y \subseteq ⋃ ran F$