Step | Hyp | Ref
| Expression |
1 | | eqeq2 2750 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐴)) |
2 | 1 | anbi2d 629 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝜑 ∧ 𝑥 = 𝑦) ↔ (𝜑 ∧ 𝑥 = 𝐴))) |
3 | | biidd 261 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))) |
4 | | biidd 261 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (𝜓 ∧ 𝑥 = 𝐶))) |
5 | 2, 3, 4 | 3orbi123d 1434 |
. . . . 5
⊢ (𝑦 = 𝐴 → (((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
6 | 5 | eubidv 2586 |
. . . 4
⊢ (𝑦 = 𝐴 → (∃!𝑥((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
7 | | vex 3436 |
. . . . 5
⊢ 𝑦 ∈ V |
8 | | moeq3.1 |
. . . . 5
⊢ 𝐵 ∈ V |
9 | | moeq3.2 |
. . . . 5
⊢ 𝐶 ∈ V |
10 | | moeq3.3 |
. . . . 5
⊢ ¬
(𝜑 ∧ 𝜓) |
11 | 7, 8, 9, 10 | eueq3 3646 |
. . . 4
⊢
∃!𝑥((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) |
12 | 6, 11 | vtoclg 3505 |
. . 3
⊢ (𝐴 ∈ V → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
13 | | eumo 2578 |
. . 3
⊢
(∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ∃*𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
14 | 12, 13 | syl 17 |
. 2
⊢ (𝐴 ∈ V → ∃*𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
15 | | eqvisset 3449 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
16 | | pm2.21 123 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ V → (𝐴 ∈ V → 𝑥 = 𝑦)) |
17 | 15, 16 | syl5 34 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V → (𝑥 = 𝐴 → 𝑥 = 𝑦)) |
18 | 17 | anim2d 612 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → ((𝜑 ∧ 𝑥 = 𝐴) → (𝜑 ∧ 𝑥 = 𝑦))) |
19 | 18 | orim1d 963 |
. . . . 5
⊢ (¬
𝐴 ∈ V → (((𝜑 ∧ 𝑥 = 𝐴) ∨ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) → ((𝜑 ∧ 𝑥 = 𝑦) ∨ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))) |
20 | | 3orass 1089 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
21 | | 3orass 1089 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((𝜑 ∧ 𝑥 = 𝑦) ∨ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
22 | 19, 20, 21 | 3imtr4g 296 |
. . . 4
⊢ (¬
𝐴 ∈ V → (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
23 | 22 | alrimiv 1930 |
. . 3
⊢ (¬
𝐴 ∈ V →
∀𝑥(((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
24 | | euimmo 2618 |
. . 3
⊢
(∀𝑥(((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) → (∃!𝑥((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ∃*𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
25 | 23, 11, 24 | mpisyl 21 |
. 2
⊢ (¬
𝐴 ∈ V →
∃*𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
26 | 14, 25 | pm2.61i 182 |
1
⊢
∃*𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) |