Theorem elovimad

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

	Ref	Expression
Hypotheses	elovimad.1	$$⊢\phi \to A\in C$$
	elovimad.2	$$⊢\phi \to B\in D$$
	elovimad.3	$$⊢\phi \to \mathrm{Fun}F$$
	elovimad.4	$$⊢\phi \to C\times D\subseteq \mathrm{dom}F$$
Assertion	elovimad	$$⊢\phi \to AFB\in F\left[C\times D\right]$$

Proof

Step	Hyp	Ref	Expression
1		elovimad.1	$$⊢\phi \to A\in C$$
2		elovimad.2	$$⊢\phi \to B\in D$$
3		elovimad.3	$$⊢\phi \to \mathrm{Fun}F$$
4		elovimad.4	$$⊢\phi \to C\times D\subseteq \mathrm{dom}F$$
5		df-ov	$$⊢AFB=F\left(⟨A,B⟩\right)$$
6	1 2	opelxpd	$$⊢\phi \to ⟨A,B⟩\in \left(C\times D\right)$$
7	4 6	sseldd	$$⊢\phi \to ⟨A,B⟩\in \mathrm{dom}F$$
8		funfvima	$$⊢\left(\mathrm{Fun}F\wedge ⟨A,B⟩\in \mathrm{dom}F\right)\to \left(⟨A,B⟩\in \left(C\times D\right)\to F\left(⟨A,B⟩\right)\in F\left[C\times D\right]\right)$$
9	3 7 8	syl2anc	$$⊢\phi \to \left(⟨A,B⟩\in \left(C\times D\right)\to F\left(⟨A,B⟩\right)\in F\left[C\times D\right]\right)$$
10	6 9	mpd	$$⊢\phi \to F\left(⟨A,B⟩\right)\in F\left[C\times D\right]$$
11	5 10	eqeltrid	$$⊢\phi \to AFB\in F\left[C\times D\right]$$