Proof of Theorem bj-sbsb
Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . 4
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (𝑥 = 𝑦 → 𝜑)) |
2 | | pm2.27 42 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 = 𝑦 → 𝜑) → 𝜑)) |
3 | 2 | anc2li 556 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 ∧ 𝜑))) |
4 | 3 | sps 2182 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → ((𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 ∧ 𝜑))) |
5 | | olc 865 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |
6 | 1, 4, 5 | syl56 36 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))) |
7 | | simpr 485 |
. . . 4
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
8 | | equs5 2462 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
9 | 8 | biimpd 228 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
10 | | orc 864 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |
11 | 7, 9, 10 | syl56 36 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))) |
12 | 6, 11 | pm2.61i 182 |
. 2
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |
13 | | sp 2180 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 → 𝜑)) |
14 | | pm3.4 807 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 → 𝜑)) |
15 | 13, 14 | jaoi 854 |
. . 3
⊢
((∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)) → (𝑥 = 𝑦 → 𝜑)) |
16 | | equs4 2418 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
17 | | 19.8a 2178 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
18 | 16, 17 | jaoi 854 |
. . 3
⊢
((∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
19 | 15, 18 | jca 512 |
. 2
⊢
((∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)) → ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
20 | 12, 19 | impbii 208 |
1
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |