Proof of Theorem bj-sbsb
| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . 4
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (𝑥 = 𝑦 → 𝜑)) |
| 2 | | pm2.27 42 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 = 𝑦 → 𝜑) → 𝜑)) |
| 3 | 2 | anc2li 555 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 ∧ 𝜑))) |
| 4 | 3 | sps 2185 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → ((𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 ∧ 𝜑))) |
| 5 | | olc 869 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |
| 6 | 1, 4, 5 | syl56 36 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))) |
| 7 | | simpr 484 |
. . . 4
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
| 8 | | equs5 2465 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
| 9 | 8 | biimpd 229 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
| 10 | | orc 868 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |
| 11 | 7, 9, 10 | syl56 36 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))) |
| 12 | 6, 11 | pm2.61i 182 |
. 2
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |
| 13 | | sp 2183 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 → 𝜑)) |
| 14 | | pm3.4 810 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 → 𝜑)) |
| 15 | 13, 14 | jaoi 858 |
. . 3
⊢
((∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)) → (𝑥 = 𝑦 → 𝜑)) |
| 16 | | equs4 2421 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
| 17 | | 19.8a 2181 |
. . . 4
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
| 18 | 16, 17 | jaoi 858 |
. . 3
⊢
((∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
| 19 | 15, 18 | jca 511 |
. 2
⊢
((∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)) → ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
| 20 | 12, 19 | impbii 209 |
1
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |