This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resmpt3

Description: Unconditional restriction of the mapping operation. (Contributed by Stefan O'Rear, 24-Jan-2015) (Proof shortened by Mario Carneiro, 22-Mar-2015)

		Ref	Expression
	Assertion	resmpt3	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		resres	⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐴 ) ↾ 𝐵 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐴 ∩ 𝐵 ) )
2		ssid	⊢ 𝐴 ⊆ 𝐴
3		resmpt	⊢ ( 𝐴 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
4	2 3	ax-mp	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
5	4	reseq1i	⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐴 ) ↾ 𝐵 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 )
6		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
7		resmpt	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 ) )
8	6 7	ax-mp	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 )
9	1 5 8	3eqtr3i	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 )