Theorem ovmpoelrn

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

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

Proof

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