Step |
Hyp |
Ref |
Expression |
1 |
|
dfcleq |
⊢ ( 𝐵 = 𝐶 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) |
2 |
1
|
sbcth |
⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 / 𝑥 ] ( 𝐵 = 𝐶 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) ) |
3 |
|
sbcbig |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝐵 = 𝐶 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ [ 𝐴 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) ) ) |
4 |
2 3
|
mpbid |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ [ 𝐴 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) ) |
5 |
|
sbcal |
⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) |
6 |
4 5
|
bitrdi |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) ) |
7 |
|
sbcbig |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ) ) |
8 |
7
|
albidv |
⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ↔ ∀ 𝑦 ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ) ) |
9 |
|
sbcel2 |
⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) |
10 |
9
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
11 |
|
sbcel2 |
⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) |
12 |
11
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) |
13 |
10 12
|
bibi12d |
⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) |
14 |
13
|
albidv |
⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) |
15 |
6 8 14
|
3bitrd |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ ∀ 𝑦 ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) |
16 |
|
dfcleq |
⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ ∀ 𝑦 ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) |
17 |
15 16
|
bitr4di |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) |