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