Step |
Hyp |
Ref |
Expression |
1 |
|
csbov123 |
⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) |
2 |
|
csbconstg |
⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵 ) |
3 |
|
csbconstg |
⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐶 ) |
4 |
2 3
|
oveq12d |
⊢ ( 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝐶 ) ) |
5 |
|
0fv |
⊢ ( ∅ ‘ 〈 𝐵 , 𝐶 〉 ) = ∅ |
6 |
|
df-ov |
⊢ ( 𝐵 ∅ 𝐶 ) = ( ∅ ‘ 〈 𝐵 , 𝐶 〉 ) |
7 |
|
0ov |
⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∅ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ∅ |
8 |
5 6 7
|
3eqtr4ri |
⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∅ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( 𝐵 ∅ 𝐶 ) |
9 |
|
csbprc |
⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ∅ ) |
10 |
9
|
oveqd |
⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∅ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) |
11 |
9
|
oveqd |
⊢ ( ¬ 𝐴 ∈ V → ( 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝐶 ) = ( 𝐵 ∅ 𝐶 ) ) |
12 |
8 10 11
|
3eqtr4a |
⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝐶 ) ) |
13 |
4 12
|
pm2.61i |
⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝐶 ) |
14 |
1 13
|
eqtri |
⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 𝐹 𝐶 ) = ( 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝐶 ) |