Step | Hyp | Ref
| Expression |
1 | | csbeq1 3139 |
. . 3
⊢ (y = A →
[y / x] if(φ, B,
C) = [A / x]
if(φ, B, C)) |
2 | | dfsbcq2 3049 |
. . . 4
⊢ (y = A →
([y / x]φ ↔
[̣A / x]̣φ)) |
3 | | csbeq1 3139 |
. . . 4
⊢ (y = A →
[y / x]B =
[A / x]B) |
4 | | csbeq1 3139 |
. . . 4
⊢ (y = A →
[y / x]C =
[A / x]C) |
5 | 2, 3, 4 | ifbieq12d 3684 |
. . 3
⊢ (y = A →
if([y / x]φ,
[y / x]B,
[y / x]C) =
if([̣A / x]̣φ,
[A / x]B,
[A / x]C)) |
6 | 1, 5 | eqeq12d 2367 |
. 2
⊢ (y = A →
([y / x] if(φ, B,
C) = if([y / x]φ, [y / x]B,
[y / x]C)
↔ [A / x] if(φ, B,
C) = if([̣A / x]̣φ,
[A / x]B,
[A / x]C))) |
7 | | vex 2862 |
. . 3
⊢ y ∈
V |
8 | | nfs1v 2106 |
. . . 4
⊢ Ⅎx[y / x]φ |
9 | | nfcsb1v 3168 |
. . . 4
⊢
Ⅎx[y / x]B |
10 | | nfcsb1v 3168 |
. . . 4
⊢
Ⅎx[y / x]C |
11 | 8, 9, 10 | nfif 3686 |
. . 3
⊢
Ⅎx if([y / x]φ, [y / x]B,
[y / x]C) |
12 | | sbequ12 1919 |
. . . 4
⊢ (x = y →
(φ ↔ [y / x]φ)) |
13 | | csbeq1a 3144 |
. . . 4
⊢ (x = y →
B = [y / x]B) |
14 | | csbeq1a 3144 |
. . . 4
⊢ (x = y →
C = [y / x]C) |
15 | 12, 13, 14 | ifbieq12d 3684 |
. . 3
⊢ (x = y →
if(φ, B, C) =
if([y / x]φ,
[y / x]B,
[y / x]C)) |
16 | 7, 11, 15 | csbief 3177 |
. 2
⊢ [y / x]
if(φ, B, C) =
if([y / x]φ,
[y / x]B,
[y / x]C) |
17 | 6, 16 | vtoclg 2914 |
1
⊢ (A ∈ V → [A / x]
if(φ, B, C) =
if([̣A / x]̣φ,
[A / x]B,
[A / x]C)) |