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