Proof of Theorem sbequi
Step | Hyp | Ref
| Expression |
1 | | nfsb2or 1715 |
. . . 4
⊢ (∀z z = x ∨ Ⅎz[x / z]φ) |
2 | | nfr 1408 |
. . . . . 6
⊢
(Ⅎz[x / z]φ → ([x / z]φ → ∀z[x / z]φ)) |
3 | | equvini 1638 |
. . . . . . 7
⊢ (x = y →
∃z(x = z ∧ z = y)) |
4 | | stdpc7 1650 |
. . . . . . . . 9
⊢ (x = z →
([x / z]φ →
φ)) |
5 | | sbequ1 1648 |
. . . . . . . . 9
⊢ (z = y →
(φ → [y / z]φ)) |
6 | 4, 5 | sylan9 389 |
. . . . . . . 8
⊢
((x = z ∧ z = y) →
([x / z]φ →
[y / z]φ)) |
7 | 6 | eximi 1488 |
. . . . . . 7
⊢ (∃z(x = z ∧ z = y) → ∃z([x / z]φ → [y / z]φ)) |
8 | | 19.35-1 1512 |
. . . . . . 7
⊢ (∃z([x / z]φ → [y / z]φ) → (∀z[x / z]φ → ∃z[y / z]φ)) |
9 | 3, 7, 8 | 3syl 17 |
. . . . . 6
⊢ (x = y →
(∀z[x / z]φ →
∃z[y / z]φ)) |
10 | 2, 9 | syl9 66 |
. . . . 5
⊢
(Ⅎz[x / z]φ → (x = y →
([x / z]φ →
∃z[y / z]φ))) |
11 | 10 | orim2i 677 |
. . . 4
⊢ ((∀z z = x ∨ Ⅎz[x / z]φ) →
(∀z
z = x
∨ (x =
y → ([x / z]φ → ∃z[y / z]φ)))) |
12 | 1, 11 | ax-mp 7 |
. . 3
⊢ (∀z z = x ∨ (x = y → ([x /
z]φ
→ ∃z[y / z]φ))) |
13 | | nfsb2or 1715 |
. . . . 5
⊢ (∀z z = y ∨ Ⅎz[y / z]φ) |
14 | | 19.9t 1530 |
. . . . . . 7
⊢
(Ⅎz[y / z]φ → (∃z[y / z]φ ↔ [y / z]φ)) |
15 | 14 | biimpd 132 |
. . . . . 6
⊢
(Ⅎz[y / z]φ → (∃z[y / z]φ → [y / z]φ)) |
16 | 15 | orim2i 677 |
. . . . 5
⊢ ((∀z z = y ∨ Ⅎz[y / z]φ) →
(∀z
z = y
∨ (∃z[y / z]φ → [y / z]φ))) |
17 | 13, 16 | ax-mp 7 |
. . . 4
⊢ (∀z z = y ∨ (∃z[y / z]φ →
[y / z]φ)) |
18 | | ax-1 5 |
. . . . 5
⊢ ((∃z[y / z]φ → [y / z]φ) → (x = y →
(∃z[y / z]φ →
[y / z]φ))) |
19 | 18 | orim2i 677 |
. . . 4
⊢ ((∀z z = y ∨ (∃z[y / z]φ →
[y / z]φ)) →
(∀z
z = y
∨ (x =
y → (∃z[y / z]φ → [y / z]φ)))) |
20 | 17, 19 | ax-mp 7 |
. . 3
⊢ (∀z z = y ∨ (x = y → (∃z[y / z]φ → [y / z]φ))) |
21 | 12, 20 | sbequilem 1716 |
. 2
⊢ (∀z z = x ∨ (∀z z = y ∨ (x = y →
([x / z]φ →
[y / z]φ)))) |
22 | | sbequ2 1649 |
. . . . . . 7
⊢ (z = x →
([x / z]φ →
φ)) |
23 | 22 | sps 1427 |
. . . . . 6
⊢ (∀z z = x →
([x / z]φ →
φ)) |
24 | 23 | adantr 261 |
. . . . 5
⊢ ((∀z z = x ∧ x = y) → ([x /
z]φ
→ φ)) |
25 | | sbequ1 1648 |
. . . . . 6
⊢ (x = y →
(φ → [y / x]φ)) |
26 | | drsb1 1677 |
. . . . . . . 8
⊢ (∀x x = z →
([y / x]φ ↔
[y / z]φ)) |
27 | 26 | biimpd 132 |
. . . . . . 7
⊢ (∀x x = z →
([y / x]φ →
[y / z]φ)) |
28 | 27 | alequcoms 1406 |
. . . . . 6
⊢ (∀z z = x →
([y / x]φ →
[y / z]φ)) |
29 | 25, 28 | sylan9r 390 |
. . . . 5
⊢ ((∀z z = x ∧ x = y) → (φ
→ [y / z]φ)) |
30 | 24, 29 | syld 40 |
. . . 4
⊢ ((∀z z = x ∧ x = y) → ([x /
z]φ
→ [y / z]φ)) |
31 | 30 | ex 108 |
. . 3
⊢ (∀z z = x →
(x = y
→ ([x / z]φ →
[y / z]φ))) |
32 | | drsb1 1677 |
. . . . . . . . 9
⊢ (∀z z = y →
([x / z]φ ↔
[x / y]φ)) |
33 | 32 | biimpd 132 |
. . . . . . . 8
⊢ (∀z z = y →
([x / z]φ →
[x / y]φ)) |
34 | | stdpc7 1650 |
. . . . . . . 8
⊢ (x = y →
([x / y]φ →
φ)) |
35 | 33, 34 | sylan9 389 |
. . . . . . 7
⊢ ((∀z z = y ∧ x = y) → ([x /
z]φ
→ φ)) |
36 | 5 | sps 1427 |
. . . . . . . 8
⊢ (∀z z = y →
(φ → [y / z]φ)) |
37 | 36 | adantr 261 |
. . . . . . 7
⊢ ((∀z z = y ∧ x = y) → (φ
→ [y / z]φ)) |
38 | 35, 37 | syld 40 |
. . . . . 6
⊢ ((∀z z = y ∧ x = y) → ([x /
z]φ
→ [y / z]φ)) |
39 | 38 | ex 108 |
. . . . 5
⊢ (∀z z = y →
(x = y
→ ([x / z]φ →
[y / z]φ))) |
40 | 39 | orim1i 676 |
. . . 4
⊢ ((∀z z = y ∨ (x = y → ([x /
z]φ
→ [y / z]φ)))
→ ((x = y → ([x /
z]φ
→ [y / z]φ)) ∨ (x = y → ([x /
z]φ
→ [y / z]φ)))) |
41 | | pm1.2 672 |
. . . 4
⊢
(((x = y → ([x /
z]φ
→ [y / z]φ)) ∨ (x = y → ([x /
z]φ
→ [y / z]φ)))
→ (x = y → ([x /
z]φ
→ [y / z]φ))) |
42 | 40, 41 | syl 14 |
. . 3
⊢ ((∀z z = y ∨ (x = y → ([x /
z]φ
→ [y / z]φ)))
→ (x = y → ([x /
z]φ
→ [y / z]φ))) |
43 | 31, 42 | jaoi 635 |
. 2
⊢ ((∀z z = x ∨ (∀z z = y ∨ (x = y →
([x / z]φ →
[y / z]φ))))
→ (x = y → ([x /
z]φ
→ [y / z]φ))) |
44 | 21, 43 | ax-mp 7 |
1
⊢ (x = y →
([x / z]φ →
[y / z]φ)) |