Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . . . . 6
⊢ ((𝑥 = 𝑡 → 𝜑) → (∃𝑦 𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
2 | | 19.23v 2023 |
. . . . . 6
⊢
(∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑)) ↔ (∃𝑦 𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
3 | 1, 2 | sylibr 224 |
. . . . 5
⊢ ((𝑥 = 𝑡 → 𝜑) → ∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
4 | | equequ2 2111 |
. . . . . . . 8
⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡)) |
5 | 4 | imbi1d 330 |
. . . . . . 7
⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑))) |
6 | 5 | pm5.74i 260 |
. . . . . 6
⊢ ((𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
7 | 6 | albii 1895 |
. . . . 5
⊢
(∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑡 → 𝜑))) |
8 | 3, 7 | sylibr 224 |
. . . 4
⊢ ((𝑥 = 𝑡 → 𝜑) → ∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑))) |
9 | 8 | alimi 1887 |
. . 3
⊢
(∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑))) |
10 | | bj-ssblem2 32962 |
. . 3
⊢
(∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑))) |
11 | | stdpc5v 2019 |
. . . 4
⊢
(∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
12 | 11 | alimi 1887 |
. . 3
⊢
(∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
13 | 9, 10, 12 | 3syl 18 |
. 2
⊢
(∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
14 | | df-ssb 32951 |
. 2
⊢ ([𝑡/𝑥]b𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
15 | 13, 14 | sylibr 224 |
1
⊢
(∀𝑥(𝑥 = 𝑡 → 𝜑) → [𝑡/𝑥]b𝜑) |