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