Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . . . . 6
⊢ ((𝑥 = 𝑡 → 𝜑) → (∃𝑦 𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
2 | | 19.23v 1889 |
. . . . . 6
⊢
(∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑)) ↔ (∃𝑦 𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
3 | 1, 2 | sylibr 223 |
. . . . 5
⊢ ((𝑥 = 𝑡 → 𝜑) → ∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
4 | | equequ2 1940 |
. . . . . . . 8
⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡)) |
5 | 4 | imbi1d 330 |
. . . . . . 7
⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑))) |
6 | 5 | pm5.74i 259 |
. . . . . 6
⊢ ((𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
7 | 6 | albii 1737 |
. . . . 5
⊢
(∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
8 | 3, 7 | sylibr 223 |
. . . 4
⊢ ((𝑥 = 𝑡 → 𝜑) → ∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑))) |
9 | 8 | alimi 1730 |
. . 3
⊢
(∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑))) |
10 | | bj-ssblem2 31820 |
. . 3
⊢
(∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑))) |
11 | | stdpc5v 1854 |
. . . 4
⊢
(∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
12 | 11 | alimi 1730 |
. . 3
⊢
(∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
13 | 9, 10, 12 | 3syl 18 |
. 2
⊢
(∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
14 | | df-ssb 31809 |
. 2
⊢ ([𝑡/𝑥]b𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
15 | 13, 14 | sylibr 223 |
1
⊢
(∀𝑥(𝑥 = 𝑡 → 𝜑) → [𝑡/𝑥]b𝜑) |