# Metamath Proof Explorer

## Theorem fmpt2d

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014)

Ref Expression
Hypotheses fmpt2d.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
fmpt2d.1 ${⊢}{\phi }\to {F}=\left({x}\in {A}⟼{B}\right)$
fmpt2d.3 ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right)\in {C}$
Assertion fmpt2d ${⊢}{\phi }\to {F}:{A}⟶{C}$

### Proof

Step Hyp Ref Expression
1 fmpt2d.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
2 fmpt2d.1 ${⊢}{\phi }\to {F}=\left({x}\in {A}⟼{B}\right)$
3 fmpt2d.3 ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right)\in {C}$
4 1 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {V}$
5 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
6 5 fnmpt ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {V}\to \left({x}\in {A}⟼{B}\right)Fn{A}$
7 4 6 syl ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)Fn{A}$
8 2 fneq1d ${⊢}{\phi }\to \left({F}Fn{A}↔\left({x}\in {A}⟼{B}\right)Fn{A}\right)$
9 7 8 mpbird ${⊢}{\phi }\to {F}Fn{A}$
10 3 ralrimiva ${⊢}{\phi }\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\in {C}$
11 ffnfv ${⊢}{F}:{A}⟶{C}↔\left({F}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\in {C}\right)$
12 9 10 11 sylanbrc ${⊢}{\phi }\to {F}:{A}⟶{C}$