Theorem elovimad

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

	Ref	Expression
Hypotheses	elovimad.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
	elovimad.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
	elovimad.3	⊢ ( 𝜑 → Fun 𝐹 )
	elovimad.4	⊢ ( 𝜑 → ( 𝐶 × 𝐷 ) ⊆ dom 𝐹 )
Assertion	elovimad	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ ( 𝐹 “ ( 𝐶 × 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elovimad.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
2		elovimad.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
3		elovimad.3	⊢ ( 𝜑 → Fun 𝐹 )
4		elovimad.4	⊢ ( 𝜑 → ( 𝐶 × 𝐷 ) ⊆ dom 𝐹 )
5		df-ov	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
6	1 2	opelxpd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) )
7	4 6	sseldd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 )
8		funfvima	⊢ ( ( Fun 𝐹 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 𝐹 “ ( 𝐶 × 𝐷 ) ) ) )
9	3 7 8	syl2anc	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 𝐹 “ ( 𝐶 × 𝐷 ) ) ) )
10	6 9	mpd	⊢ ( 𝜑 → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 𝐹 “ ( 𝐶 × 𝐷 ) ) )
11	5 10	eqeltrid	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ ( 𝐹 “ ( 𝐶 × 𝐷 ) ) )