Proof of Theorem eueq2dc
Step | Hyp | Ref
| Expression |
1 | | df-dc 821 |
. 2
⊢
(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) |
2 | | notnot 619 |
. . . . 5
⊢ (𝜑 → ¬ ¬ 𝜑) |
3 | | eueq2dc.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
4 | 3 | eueq1 2884 |
. . . . . 6
⊢
∃!𝑥 𝑥 = 𝐴 |
5 | | euanv 2063 |
. . . . . . 7
⊢
(∃!𝑥(𝜑 ∧ 𝑥 = 𝐴) ↔ (𝜑 ∧ ∃!𝑥 𝑥 = 𝐴)) |
6 | 5 | biimpri 132 |
. . . . . 6
⊢ ((𝜑 ∧ ∃!𝑥 𝑥 = 𝐴) → ∃!𝑥(𝜑 ∧ 𝑥 = 𝐴)) |
7 | 4, 6 | mpan2 422 |
. . . . 5
⊢ (𝜑 → ∃!𝑥(𝜑 ∧ 𝑥 = 𝐴)) |
8 | | euorv 2033 |
. . . . 5
⊢ ((¬
¬ 𝜑 ∧ ∃!𝑥(𝜑 ∧ 𝑥 = 𝐴)) → ∃!𝑥(¬ 𝜑 ∨ (𝜑 ∧ 𝑥 = 𝐴))) |
9 | 2, 7, 8 | syl2anc 409 |
. . . 4
⊢ (𝜑 → ∃!𝑥(¬ 𝜑 ∨ (𝜑 ∧ 𝑥 = 𝐴))) |
10 | | orcom 718 |
. . . . . 6
⊢ ((¬
𝜑 ∨ (𝜑 ∧ 𝑥 = 𝐴)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ ¬ 𝜑)) |
11 | 2 | bianfd 933 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝜑 ↔ (¬ 𝜑 ∧ 𝑥 = 𝐵))) |
12 | 11 | orbi2d 780 |
. . . . . 6
⊢ (𝜑 → (((𝜑 ∧ 𝑥 = 𝐴) ∨ ¬ 𝜑) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵)))) |
13 | 10, 12 | syl5bb 191 |
. . . . 5
⊢ (𝜑 → ((¬ 𝜑 ∨ (𝜑 ∧ 𝑥 = 𝐴)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵)))) |
14 | 13 | eubidv 2014 |
. . . 4
⊢ (𝜑 → (∃!𝑥(¬ 𝜑 ∨ (𝜑 ∧ 𝑥 = 𝐴)) ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵)))) |
15 | 9, 14 | mpbid 146 |
. . 3
⊢ (𝜑 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵))) |
16 | | eueq2dc.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
17 | 16 | eueq1 2884 |
. . . . . 6
⊢
∃!𝑥 𝑥 = 𝐵 |
18 | | euanv 2063 |
. . . . . . 7
⊢
(∃!𝑥(¬
𝜑 ∧ 𝑥 = 𝐵) ↔ (¬ 𝜑 ∧ ∃!𝑥 𝑥 = 𝐵)) |
19 | 18 | biimpri 132 |
. . . . . 6
⊢ ((¬
𝜑 ∧ ∃!𝑥 𝑥 = 𝐵) → ∃!𝑥(¬ 𝜑 ∧ 𝑥 = 𝐵)) |
20 | 17, 19 | mpan2 422 |
. . . . 5
⊢ (¬
𝜑 → ∃!𝑥(¬ 𝜑 ∧ 𝑥 = 𝐵)) |
21 | | euorv 2033 |
. . . . 5
⊢ ((¬
𝜑 ∧ ∃!𝑥(¬ 𝜑 ∧ 𝑥 = 𝐵)) → ∃!𝑥(𝜑 ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵))) |
22 | 20, 21 | mpdan 418 |
. . . 4
⊢ (¬
𝜑 → ∃!𝑥(𝜑 ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵))) |
23 | | id 19 |
. . . . . . 7
⊢ (¬
𝜑 → ¬ 𝜑) |
24 | 23 | bianfd 933 |
. . . . . 6
⊢ (¬
𝜑 → (𝜑 ↔ (𝜑 ∧ 𝑥 = 𝐴))) |
25 | 24 | orbi1d 781 |
. . . . 5
⊢ (¬
𝜑 → ((𝜑 ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵)))) |
26 | 25 | eubidv 2014 |
. . . 4
⊢ (¬
𝜑 → (∃!𝑥(𝜑 ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵)) ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵)))) |
27 | 22, 26 | mpbid 146 |
. . 3
⊢ (¬
𝜑 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵))) |
28 | 15, 27 | jaoi 706 |
. 2
⊢ ((𝜑 ∨ ¬ 𝜑) → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵))) |
29 | 1, 28 | sylbi 120 |
1
⊢
(DECID 𝜑 → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 = 𝐵))) |