Theorem elovimad

Description: Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017)

	Ref	Expression
Hypotheses	elovimad.1	|- ( ph -> A e. C )
	elovimad.2	|- ( ph -> B e. D )
	elovimad.3	|- ( ph -> Fun F )
	elovimad.4	|- ( ph -> ( C X. D ) C_ dom F )
Assertion	elovimad	|- ( ph -> ( A F B ) e. ( F " ( C X. D ) ) )

Proof

Step	Hyp	Ref	Expression
1		elovimad.1	|- ( ph -> A e. C )
2		elovimad.2	|- ( ph -> B e. D )
3		elovimad.3	|- ( ph -> Fun F )
4		elovimad.4	|- ( ph -> ( C X. D ) C_ dom F )
5		df-ov	|- ( A F B ) = ( F ` <. A , B >. )
6	1 2	opelxpd	|- ( ph -> <. A , B >. e. ( C X. D ) )
7	4 6	sseldd	|- ( ph -> <. A , B >. e. dom F )
8		funfvima	|- ( ( Fun F /\ <. A , B >. e. dom F ) -> ( <. A , B >. e. ( C X. D ) -> ( F ` <. A , B >. ) e. ( F " ( C X. D ) ) ) )
9	3 7 8	syl2anc	|- ( ph -> ( <. A , B >. e. ( C X. D ) -> ( F ` <. A , B >. ) e. ( F " ( C X. D ) ) ) )
10	6 9	mpd	|- ( ph -> ( F ` <. A , B >. ) e. ( F " ( C X. D ) ) )
11	5 10	eqeltrid	|- ( ph -> ( A F B ) e. ( F " ( C X. D ) ) )