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

Metamath Proof Explorer

Theorem resmptf

Description: Restriction of the mapping operation. (Contributed by Thierry Arnoux, 28-Mar-2017)

Ref Expression
Hypotheses resmptf.a ⊢ Ⅎ 𝑥 𝐴
resmptf.b ⊢ Ⅎ 𝑥 𝐵
Assertion resmptf ( 𝐵 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 resmptf.a ⊢ Ⅎ 𝑥 𝐴
2 resmptf.b ⊢ Ⅎ 𝑥 𝐵
3 resmpt ⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ↾ 𝐵 ) = ( 𝑦 ∈ 𝐵 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
4 nfcv ⊢ Ⅎ 𝑦 𝐴
5 nfcv ⊢ Ⅎ 𝑦 𝐶
6 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
7 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
8 1 4 5 6 7 cbvmptf ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
9 8 reseq1i ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 ) = ( ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ↾ 𝐵 )
10 nfcv ⊢ Ⅎ 𝑦 𝐵
11 2 10 5 6 7 cbvmptf ⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
12 3 9 11 3eqtr4g ⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )