This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elovimad

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

Ref Expression
Hypotheses elovimad.1 ⊢ φ → A ∈ C
elovimad.2 ⊢ φ → B ∈ D
elovimad.3 ⊢ φ → Fun ⁡ F
elovimad.4 ⊢ φ → C × D ⊆ dom ⁡ F
Assertion elovimad ⊢ φ → A F B ∈ F C × D

Proof

Step Hyp Ref Expression
1 elovimad.1 ⊢ φ → A ∈ C
2 elovimad.2 ⊢ φ → B ∈ D
3 elovimad.3 ⊢ φ → Fun ⁡ F
4 elovimad.4 ⊢ φ → C × D ⊆ dom ⁡ F
5 df-ov ⊢ A F B = F ⁡ A B
6 1 2 opelxpd ⊢ φ → A B ∈ C × D
7 4 6 sseldd ⊢ φ → A B ∈ dom ⁡ F
8 funfvima ⊢ Fun ⁡ F ∧ A B ∈ dom ⁡ F → A B ∈ C × D → F ⁡ A B ∈ F C × D
9 3 7 8 syl2anc ⊢ φ → A B ∈ C × D → F ⁡ A B ∈ F C × D
10 6 9 mpd ⊢ φ → F ⁡ A B ∈ F C × D
11 5 10 eqeltrid ⊢ φ → A F B ∈ F C × D