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 ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↾ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )

Proof

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