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 ⊢ Ⅎ _ x A
resmptf.b ⊢ Ⅎ _ x B
Assertion resmptf ⊢ B ⊆ A → x ∈ A ⟼ C ↾ B = x ∈ B ⟼ C

Proof

Step Hyp Ref Expression
1 resmptf.a ⊢ Ⅎ _ x A
2 resmptf.b ⊢ Ⅎ _ x B
3 resmpt ⊢ B ⊆ A → y ∈ A ⟼ ⦋ y / x⦌ C ↾ B = y ∈ B ⟼ ⦋ y / x⦌ C
4 nfcv ⊢ Ⅎ _ y A
5 nfcv ⊢ Ⅎ _ y C
6 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ C
7 csbeq1a ⊢ x = y → C = ⦋ y / x⦌ C
8 1 4 5 6 7 cbvmptf ⊢ x ∈ A ⟼ C = y ∈ A ⟼ ⦋ y / x⦌ C
9 8 reseq1i ⊢ x ∈ A ⟼ C ↾ B = y ∈ A ⟼ ⦋ y / x⦌ C ↾ B
10 nfcv ⊢ Ⅎ _ y B
11 2 10 5 6 7 cbvmptf ⊢ x ∈ B ⟼ C = y ∈ B ⟼ ⦋ y / x⦌ C
12 3 9 11 3eqtr4g ⊢ B ⊆ A → x ∈ A ⟼ C ↾ B = x ∈ B ⟼ C