Step | Hyp | Ref
| Expression |
1 | | elex 2867 |
. 2
⊢ (A ∈ V → A ∈ V) |
2 | | elex 2867 |
. 2
⊢ (B ∈ W → B ∈ V) |
3 | | sbccom 3117 |
. . . . . 6
⊢ ([̣A / x]̣[̣B
/ y]̣z ∈ C ↔ [̣B / y]̣[̣A
/ x]̣z ∈ C) |
4 | 3 | a1i 10 |
. . . . 5
⊢ ((A ∈ V ∧ B ∈ V) → ([̣A / x]̣[̣B
/ y]̣z ∈ C ↔ [̣B / y]̣[̣A
/ x]̣z ∈ C)) |
5 | | sbcel2g 3157 |
. . . . . . 7
⊢ (B ∈ V →
([̣B / y]̣z ∈ C ↔
z ∈
[B / y]C)) |
6 | 5 | sbcbidv 3100 |
. . . . . 6
⊢ (B ∈ V →
([̣A / x]̣[̣B
/ y]̣z ∈ C ↔ [̣A / x]̣z ∈ [B /
y]C)) |
7 | 6 | adantl 452 |
. . . . 5
⊢ ((A ∈ V ∧ B ∈ V) → ([̣A / x]̣[̣B
/ y]̣z ∈ C ↔ [̣A / x]̣z ∈ [B /
y]C)) |
8 | | sbcel2g 3157 |
. . . . . . 7
⊢ (A ∈ V →
([̣A / x]̣z ∈ C ↔
z ∈
[A / x]C)) |
9 | 8 | sbcbidv 3100 |
. . . . . 6
⊢ (A ∈ V →
([̣B / y]̣[̣A
/ x]̣z ∈ C ↔ [̣B / y]̣z ∈ [A /
x]C)) |
10 | 9 | adantr 451 |
. . . . 5
⊢ ((A ∈ V ∧ B ∈ V) → ([̣B / y]̣[̣A
/ x]̣z ∈ C ↔ [̣B / y]̣z ∈ [A /
x]C)) |
11 | 4, 7, 10 | 3bitr3d 274 |
. . . 4
⊢ ((A ∈ V ∧ B ∈ V) → ([̣A / x]̣z ∈ [B /
y]C ↔ [̣B / y]̣z ∈ [A /
x]C)) |
12 | | sbcel2g 3157 |
. . . . 5
⊢ (A ∈ V →
([̣A / x]̣z ∈ [B /
y]C ↔ z ∈ [A /
x][B / y]C)) |
13 | 12 | adantr 451 |
. . . 4
⊢ ((A ∈ V ∧ B ∈ V) → ([̣A / x]̣z ∈ [B /
y]C ↔ z ∈ [A /
x][B / y]C)) |
14 | | sbcel2g 3157 |
. . . . 5
⊢ (B ∈ V →
([̣B / y]̣z ∈ [A /
x]C ↔ z ∈ [B /
y][A / x]C)) |
15 | 14 | adantl 452 |
. . . 4
⊢ ((A ∈ V ∧ B ∈ V) → ([̣B / y]̣z ∈ [A /
x]C ↔ z ∈ [B /
y][A / x]C)) |
16 | 11, 13, 15 | 3bitr3d 274 |
. . 3
⊢ ((A ∈ V ∧ B ∈ V) → (z
∈ [A / x][B / y]C
↔ z ∈ [B /
y][A / x]C)) |
17 | 16 | eqrdv 2351 |
. 2
⊢ ((A ∈ V ∧ B ∈ V) → [A / x][B / y]C =
[B / y][A / x]C) |
18 | 1, 2, 17 | syl2an 463 |
1
⊢ ((A ∈ V ∧ B ∈ W) → [A / x][B / y]C =
[B / y][A / x]C) |