Proof of Theorem drex1
Step | Hyp | Ref
| Expression |
1 | | hbae 1603 |
. . . 4
⊢ (∀x x = y →
∀x∀x x = y) |
2 | | drex1.1 |
. . . . 5
⊢ (∀x x = y →
(φ ↔ ψ)) |
3 | | ax-4 1397 |
. . . . . 6
⊢ (∀x x = y →
x = y) |
4 | 3 | biantrurd 289 |
. . . . 5
⊢ (∀x x = y →
(ψ ↔ (x = y ∧ ψ))) |
5 | 2, 4 | bitr2d 178 |
. . . 4
⊢ (∀x x = y →
((x = y
∧ ψ)
↔ φ)) |
6 | 1, 5 | exbidh 1502 |
. . 3
⊢ (∀x x = y →
(∃x(x = y ∧ ψ) ↔ ∃xφ)) |
7 | | ax11e 1674 |
. . . 4
⊢ (x = y →
(∃x(x = y ∧ ψ) → ∃yψ)) |
8 | 7 | sps 1427 |
. . 3
⊢ (∀x x = y →
(∃x(x = y ∧ ψ) → ∃yψ)) |
9 | 6, 8 | sylbird 159 |
. 2
⊢ (∀x x = y →
(∃xφ → ∃yψ)) |
10 | | hbae 1603 |
. . . 4
⊢ (∀x x = y →
∀y∀x x = y) |
11 | | equcomi 1589 |
. . . . . . 7
⊢ (x = y →
y = x) |
12 | 11 | sps 1427 |
. . . . . 6
⊢ (∀x x = y →
y = x) |
13 | 12 | biantrurd 289 |
. . . . 5
⊢ (∀x x = y →
(φ ↔ (y = x ∧ φ))) |
14 | 13, 2 | bitr3d 179 |
. . . 4
⊢ (∀x x = y →
((y = x
∧ φ)
↔ ψ)) |
15 | 10, 14 | exbidh 1502 |
. . 3
⊢ (∀x x = y →
(∃y(y = x ∧ φ) ↔ ∃yψ)) |
16 | | ax11e 1674 |
. . . . 5
⊢ (y = x →
(∃y(y = x ∧ φ) → ∃xφ)) |
17 | 16 | sps 1427 |
. . . 4
⊢ (∀y y = x →
(∃y(y = x ∧ φ) → ∃xφ)) |
18 | 17 | alequcoms 1406 |
. . 3
⊢ (∀x x = y →
(∃y(y = x ∧ φ) → ∃xφ)) |
19 | 15, 18 | sylbird 159 |
. 2
⊢ (∀x x = y →
(∃yψ → ∃xφ)) |
20 | 9, 19 | impbid 120 |
1
⊢ (∀x x = y →
(∃xφ ↔ ∃yψ)) |