Step |
Hyp |
Ref |
Expression |
1 |
|
vtocl2dOLD.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
2 |
|
vtocl2dOLD.b |
⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) |
3 |
|
vtocl2dOLD.1 |
⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) ) |
4 |
|
vtocl2dOLD.3 |
⊢ ( 𝜑 → 𝜓 ) |
5 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐵 |
6 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐵 |
7 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐴 |
8 |
|
nfv |
⊢ Ⅎ 𝑦 𝜑 |
9 |
|
nfsbc1v |
⊢ Ⅎ 𝑦 [ 𝐵 / 𝑦 ] 𝜓 |
10 |
8 9
|
nfim |
⊢ Ⅎ 𝑦 ( 𝜑 → [ 𝐵 / 𝑦 ] 𝜓 ) |
11 |
|
nfv |
⊢ Ⅎ 𝑥 ( 𝜑 → 𝜒 ) |
12 |
|
sbceq1a |
⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ [ 𝐵 / 𝑦 ] 𝜓 ) ) |
13 |
12
|
imbi2d |
⊢ ( 𝑦 = 𝐵 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → [ 𝐵 / 𝑦 ] 𝜓 ) ) ) |
14 |
|
sbceq1a |
⊢ ( 𝑥 = 𝐴 → ( [ 𝐵 / 𝑦 ] 𝜓 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜓 ) ) |
15 |
|
nfv |
⊢ Ⅎ 𝑥 𝜒 |
16 |
|
nfv |
⊢ Ⅎ 𝑦 𝜒 |
17 |
|
nfv |
⊢ Ⅎ 𝑥 𝐵 ∈ 𝑊 |
18 |
15 16 17 3
|
sbc2iegf |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) ) |
19 |
1 2 18
|
syl2anc |
⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) ) |
20 |
14 19
|
sylan9bb |
⊢ ( ( 𝑥 = 𝐴 ∧ 𝜑 ) → ( [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) ) |
21 |
20
|
pm5.74da |
⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 → [ 𝐵 / 𝑦 ] 𝜓 ) ↔ ( 𝜑 → 𝜒 ) ) ) |
22 |
5 6 7 10 11 13 21 4
|
vtocl2gf |
⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( 𝜑 → 𝜒 ) ) |
23 |
2 1 22
|
syl2anc |
⊢ ( 𝜑 → ( 𝜑 → 𝜒 ) ) |
24 |
23
|
pm2.43i |
⊢ ( 𝜑 → 𝜒 ) |