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

Metamath Proof Explorer

Theorem ovmpoelrn

Description: An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020)

		Ref	Expression
	Hypothesis	ovmpoelrn.o	$⊢ O = (x \in A, y \in B ⟼ C)$
	Assertion	ovmpoelrn	$⊢ (\forall x \in A \forall y \in B C \in M \land X \in A \land Y \in B) \to X O Y \in M$

Step	Hyp	Ref	Expression
1		ovmpoelrn.o	$⊢ O = (x \in A, y \in B ⟼ C)$
2	1	fmpo	$⊢ \forall x \in A \forall y \in B C \in M \leftrightarrow O : A \times B ⟶ M$
3		fovcdm	$⊢ (O : A \times B ⟶ M \land X \in A \land Y \in B) \to X O Y \in M$
4	2 3	syl3an1b	$⊢ (\forall x \in A \forall y \in B C \in M \land X \in A \land Y \in B) \to X O Y \in M$