Theorem resmpt

Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013)

	Ref	Expression
Assertion	resmpt	⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		resopab2	⊢ ( 𝐵 ⊆ 𝐴 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } ↾ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) } )
2		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) }
3	2	reseq1i	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) } ↾ 𝐵 )
4		df-mpt	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) }
5	1 3 4	3eqtr4g	⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )