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

Metamath Proof Explorer

Theorem csbres

Description: Distribute proper substitution through the restriction of a class. (Contributed by Alan Sare, 10-Nov-2012) (Revised by NM, 23-Aug-2018)

Ref Expression
Assertion csbres ⊢ ⦋ A / x⦌ B ↾ C = ⦋ A / x⦌ B ↾ ⦋ A / x⦌ C

Proof

Step Hyp Ref Expression
1 df-res ⊢ B ↾ C = B ∩ C × V
2 1 csbeq2i ⊢ ⦋ A / x⦌ B ↾ C = ⦋ A / x⦌ B ∩ C × V
3 csbxp ⊢ ⦋ A / x⦌ C × V = ⦋ A / x⦌ C × ⦋ A / x⦌ V
4 csbconstg ⊢ A ∈ V → ⦋ A / x⦌ V = V
5 4 xpeq2d ⊢ A ∈ V → ⦋ A / x⦌ C × ⦋ A / x⦌ V = ⦋ A / x⦌ C × V
6 3 5 eqtrid ⊢ A ∈ V → ⦋ A / x⦌ C × V = ⦋ A / x⦌ C × V
7 0xp ⊢ ∅ × V = ∅
8 7 a1i ⊢ ¬ A ∈ V → ∅ × V = ∅
9 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ C = ∅
10 9 xpeq1d ⊢ ¬ A ∈ V → ⦋ A / x⦌ C × V = ∅ × V
11 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ C × V = ∅
12 8 10 11 3eqtr4rd ⊢ ¬ A ∈ V → ⦋ A / x⦌ C × V = ⦋ A / x⦌ C × V
13 6 12 pm2.61i ⊢ ⦋ A / x⦌ C × V = ⦋ A / x⦌ C × V
14 13 ineq2i ⊢ ⦋ A / x⦌ B ∩ ⦋ A / x⦌ C × V = ⦋ A / x⦌ B ∩ ⦋ A / x⦌ C × V
15 csbin ⊢ ⦋ A / x⦌ B ∩ C × V = ⦋ A / x⦌ B ∩ ⦋ A / x⦌ C × V
16 df-res ⊢ ⦋ A / x⦌ B ↾ ⦋ A / x⦌ C = ⦋ A / x⦌ B ∩ ⦋ A / x⦌ C × V
17 14 15 16 3eqtr4i ⊢ ⦋ A / x⦌ B ∩ C × V = ⦋ A / x⦌ B ↾ ⦋ A / x⦌ C
18 2 17 eqtri ⊢ ⦋ A / x⦌ B ↾ C = ⦋ A / x⦌ B ↾ ⦋ A / x⦌ C