Step | Hyp | Ref
| Expression |
1 | | elex 2560 |
. 2
⊢ (A ∈ 𝑉 → A ∈
V) |
2 | | elex 2560 |
. 2
⊢ (B ∈ 𝑊 → B ∈
V) |
3 | | sbccom 2827 |
. . . . . 6
⊢
([A / x][B / y]z ∈ 𝐶 ↔ [B / y][A / x]z ∈ 𝐶) |
4 | 3 | a1i 9 |
. . . . 5
⊢
((A ∈ V ∧ B ∈ V) →
([A / x][B / y]z ∈ 𝐶 ↔ [B / y][A / x]z ∈ 𝐶)) |
5 | | sbcel2g 2865 |
. . . . . . 7
⊢ (B ∈ V →
([B / y]z ∈ 𝐶 ↔ z ∈
⦋B / y⦌𝐶)) |
6 | 5 | sbcbidv 2811 |
. . . . . 6
⊢ (B ∈ V →
([A / x][B / y]z ∈ 𝐶 ↔ [A / x]z ∈ ⦋B / y⦌𝐶)) |
7 | 6 | adantl 262 |
. . . . 5
⊢
((A ∈ V ∧ B ∈ V) →
([A / x][B / y]z ∈ 𝐶 ↔ [A / x]z ∈ ⦋B / y⦌𝐶)) |
8 | | sbcel2g 2865 |
. . . . . . 7
⊢ (A ∈ V →
([A / x]z ∈ 𝐶 ↔ z ∈
⦋A / x⦌𝐶)) |
9 | 8 | sbcbidv 2811 |
. . . . . 6
⊢ (A ∈ V →
([B / y][A / x]z ∈ 𝐶 ↔ [B / y]z ∈ ⦋A / x⦌𝐶)) |
10 | 9 | adantr 261 |
. . . . 5
⊢
((A ∈ V ∧ B ∈ V) →
([B / y][A / x]z ∈ 𝐶 ↔ [B / y]z ∈ ⦋A / x⦌𝐶)) |
11 | 4, 7, 10 | 3bitr3d 207 |
. . . 4
⊢
((A ∈ V ∧ B ∈ V) →
([A / x]z ∈ ⦋B / y⦌𝐶 ↔ [B / y]z ∈ ⦋A / x⦌𝐶)) |
12 | | sbcel2g 2865 |
. . . . 5
⊢ (A ∈ V →
([A / x]z ∈ ⦋B / y⦌𝐶 ↔ z ∈
⦋A / x⦌⦋B / y⦌𝐶)) |
13 | 12 | adantr 261 |
. . . 4
⊢
((A ∈ V ∧ B ∈ V) →
([A / x]z ∈ ⦋B / y⦌𝐶 ↔ z ∈
⦋A / x⦌⦋B / y⦌𝐶)) |
14 | | sbcel2g 2865 |
. . . . 5
⊢ (B ∈ V →
([B / y]z ∈ ⦋A / x⦌𝐶 ↔ z ∈
⦋B / y⦌⦋A / x⦌𝐶)) |
15 | 14 | adantl 262 |
. . . 4
⊢
((A ∈ V ∧ B ∈ V) →
([B / y]z ∈ ⦋A / x⦌𝐶 ↔ z ∈
⦋B / y⦌⦋A / x⦌𝐶)) |
16 | 11, 13, 15 | 3bitr3d 207 |
. . 3
⊢
((A ∈ V ∧ B ∈ V) →
(z ∈
⦋A / x⦌⦋B / y⦌𝐶 ↔ z ∈
⦋B / y⦌⦋A / x⦌𝐶)) |
17 | 16 | eqrdv 2035 |
. 2
⊢
((A ∈ V ∧ B ∈ V) →
⦋A / x⦌⦋B / y⦌𝐶 = ⦋B / y⦌⦋A / x⦌𝐶) |
18 | 1, 2, 17 | syl2an 273 |
1
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → ⦋A / x⦌⦋B / y⦌𝐶 = ⦋B / y⦌⦋A / x⦌𝐶) |