Theorem ovmpoelrn

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

	Ref	Expression
Hypothesis	ovmpoelrn.o	|- O = ( x e. A , y e. B |-> C )
Assertion	ovmpoelrn	|- ( ( A. x e. A A. y e. B C e. M /\ X e. A /\ Y e. B ) -> ( X O Y ) e. M )

Proof

Step	Hyp	Ref	Expression
1		ovmpoelrn.o	|- O = ( x e. A , y e. B |-> C )
2	1	fmpo	|- ( A. x e. A A. y e. B C e. M <-> O : ( A X. B ) --> M )
3		fovrn	|- ( ( O : ( A X. B ) --> M /\ X e. A /\ Y e. B ) -> ( X O Y ) e. M )
4	2 3	syl3an1b	|- ( ( A. x e. A A. y e. B C e. M /\ X e. A /\ Y e. B ) -> ( X O Y ) e. M )