Step |
Hyp |
Ref |
Expression |
1 |
|
csbiota |
⊢ ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝐵 𝐹 𝑦 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝐵 𝐹 𝑦 ) |
2 |
|
sbcbr123 |
⊢ ( [ 𝐴 / 𝑥 ] 𝐵 𝐹 𝑦 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ) |
3 |
|
csbconstg |
⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 ) |
4 |
3
|
breq2d |
⊢ ( 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 ) ) |
5 |
2 4
|
syl5bb |
⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝐵 𝐹 𝑦 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 ) ) |
6 |
5
|
iotabidv |
⊢ ( 𝐴 ∈ V → ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝐵 𝐹 𝑦 ) = ( ℩ 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 ) ) |
7 |
1 6
|
eqtrid |
⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝐵 𝐹 𝑦 ) = ( ℩ 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 ) ) |
8 |
|
df-fv |
⊢ ( 𝐹 ‘ 𝐵 ) = ( ℩ 𝑦 𝐵 𝐹 𝑦 ) |
9 |
8
|
csbeq2i |
⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝐵 𝐹 𝑦 ) |
10 |
|
df-fv |
⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ( ℩ 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 ) |
11 |
7 9 10
|
3eqtr4g |
⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
12 |
|
csbprc |
⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ∅ ) |
13 |
|
csbprc |
⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ∅ ) |
14 |
13
|
fveq1d |
⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ( ∅ ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
15 |
|
0fv |
⊢ ( ∅ ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ∅ |
16 |
14 15
|
eqtr2di |
⊢ ( ¬ 𝐴 ∈ V → ∅ = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
17 |
12 16
|
eqtrd |
⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
18 |
11 17
|
pm2.61i |
⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) |