Theorem fmptd

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013)

	Ref	Expression
Hypotheses	fmptd.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
	fmptd.2	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	fmptd	$$⊢\phi \to F:A⟶C$$

Proof

Step	Hyp	Ref	Expression
1		fmptd.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
2		fmptd.2	$$⊢F=\left(x\in A⟼B\right)$$
3	1	ralrimiva	$$⊢\phi \to \forall x\in AB\in C$$
4	2	fmpt	$$⊢\forall x\in AB\in C\leftrightarrow F:A⟶C$$
5	3 4	sylib	$$⊢\phi \to F:A⟶C$$