Proof of Theorem sbequ8
Step | Hyp | Ref
| Expression |
1 | | pm5.4 247 |
. . 3
⊢ ((𝑥 = 𝑦 → (𝑥 = 𝑦 → 𝜑)) ↔ (𝑥 = 𝑦 → 𝜑)) |
2 | | simpl 107 |
. . . . . 6
⊢ ((𝑥 = 𝑦 ∧ (𝑥 = 𝑦 → 𝜑)) → 𝑥 = 𝑦) |
3 | | pm3.35 339 |
. . . . . 6
⊢ ((𝑥 = 𝑦 ∧ (𝑥 = 𝑦 → 𝜑)) → 𝜑) |
4 | 2, 3 | jca 300 |
. . . . 5
⊢ ((𝑥 = 𝑦 ∧ (𝑥 = 𝑦 → 𝜑)) → (𝑥 = 𝑦 ∧ 𝜑)) |
5 | | simpl 107 |
. . . . . 6
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦) |
6 | | pm3.4 326 |
. . . . . 6
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 → 𝜑)) |
7 | 5, 6 | jca 300 |
. . . . 5
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 ∧ (𝑥 = 𝑦 → 𝜑))) |
8 | 4, 7 | impbii 124 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ (𝑥 = 𝑦 → 𝜑)) ↔ (𝑥 = 𝑦 ∧ 𝜑)) |
9 | 8 | exbii 1536 |
. . 3
⊢
(∃𝑥(𝑥 = 𝑦 ∧ (𝑥 = 𝑦 → 𝜑)) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
10 | 1, 9 | anbi12i 447 |
. 2
⊢ (((𝑥 = 𝑦 → (𝑥 = 𝑦 → 𝜑)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝑥 = 𝑦 → 𝜑))) ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
11 | | df-sb 1686 |
. 2
⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑) ↔ ((𝑥 = 𝑦 → (𝑥 = 𝑦 → 𝜑)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝑥 = 𝑦 → 𝜑)))) |
12 | | df-sb 1686 |
. 2
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
13 | 10, 11, 12 | 3bitr4ri 211 |
1
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑)) |