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	⊢ ( ( 𝑡 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 → ( 𝑡 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑡 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑡 ∈ 𝐴 ↦ 𝐵 )
2	1	fmpt	⊢ ( ∀ 𝑡 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ ( 𝑡 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
3		rsp	⊢ ( ∀ 𝑡 ∈ 𝐴 𝐵 ∈ 𝐶 → ( 𝑡 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) )
4	2 3	sylbir	⊢ ( ( 𝑡 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 → ( 𝑡 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) )