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 AB\in V$$
5		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
6	5	fnmpt	$$⊢\forall x\in AB\in V\to \left(x\in A⟼B\right)FnA$$
7	4 6	syl	$$⊢\phi \to \left(x\in A⟼B\right)FnA$$
8	2	fneq1d	$$⊢\phi \to \left(FFnA\leftrightarrow \left(x\in A⟼B\right)FnA\right)$$
9	7 8	mpbird	$$⊢\phi \to FFnA$$
10	3	ralrimiva	$$⊢\phi \to \forall y\in AF\left(y\right)\in C$$
11		ffnfv	$$⊢F:A⟶C\leftrightarrow \left(FFnA\wedge \forall y\in AF\left(y\right)\in C\right)$$
12	9 10 11	sylanbrc	$$⊢\phi \to F:A⟶C$$