Proof of Theorem bj-sbsb
Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . 4
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (𝑥 = 𝑦 → 𝜑)) |
2 | | pm2.27 42 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 = 𝑦 → 𝜑) → 𝜑)) |
3 | 2 | anc2li 580 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 ∧ 𝜑))) |
4 | 3 | sps 2055 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → ((𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 ∧ 𝜑))) |
5 | | olc 399 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |
6 | 1, 4, 5 | syl56 36 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))) |
7 | | simpr 477 |
. . . 4
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
8 | | equs5 2351 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
9 | 8 | biimpd 219 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
10 | | orc 400 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |
11 | 7, 9, 10 | syl56 36 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))) |
12 | 6, 11 | pm2.61i 176 |
. 2
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |
13 | | sp 2053 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 → 𝜑)) |
14 | | pm3.4 584 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 → 𝜑)) |
15 | 13, 14 | jaoi 394 |
. . 3
⊢
((∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)) → (𝑥 = 𝑦 → 𝜑)) |
16 | | equs4 2290 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
17 | | 19.8a 2052 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
18 | 16, 17 | jaoi 394 |
. . 3
⊢
((∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
19 | 15, 18 | jca 554 |
. 2
⊢
((∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)) → ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
20 | 12, 19 | impbii 199 |
1
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |