Theorem mptfcl

Description: Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014)

	Ref	Expression
Assertion	mptfcl	$$⊢\left(t\in A⟼B\right):A⟶C\to \left(t\in A\to B\in C\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(t\in A⟼B\right)=\left(t\in A⟼B\right)$$
2	1	fmpt	$$⊢\forall t\in AB\in C\leftrightarrow \left(t\in A⟼B\right):A⟶C$$
3		rsp	$$⊢\forall t\in AB\in C\to \left(t\in A\to B\in C\right)$$
4	2 3	sylbir	$$⊢\left(t\in A⟼B\right):A⟶C\to \left(t\in A\to B\in C\right)$$