| Step | Hyp | Ref
| Expression |
| 1 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐴)) |
| 2 | 1 | anbi2d 630 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝜑 ∧ 𝑥 = 𝑦) ↔ (𝜑 ∧ 𝑥 = 𝐴))) |
| 3 | | biidd 262 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ↔ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵))) |
| 4 | | biidd 262 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝜓 ∧ 𝑥 = 𝐶) ↔ (𝜓 ∧ 𝑥 = 𝐶))) |
| 5 | 2, 3, 4 | 3orbi123d 1437 |
. . . . 5
⊢ (𝑦 = 𝐴 → (((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
| 6 | 5 | eubidv 2586 |
. . . 4
⊢ (𝑦 = 𝐴 → (∃!𝑥((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
| 7 | | vex 3484 |
. . . . 5
⊢ 𝑦 ∈ V |
| 8 | | moeq3.1 |
. . . . 5
⊢ 𝐵 ∈ V |
| 9 | | moeq3.2 |
. . . . 5
⊢ 𝐶 ∈ V |
| 10 | | moeq3.3 |
. . . . 5
⊢ ¬
(𝜑 ∧ 𝜓) |
| 11 | 7, 8, 9, 10 | eueq3 3717 |
. . . 4
⊢
∃!𝑥((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) |
| 12 | 6, 11 | vtoclg 3554 |
. . 3
⊢ (𝐴 ∈ V → ∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
| 13 | | eumo 2578 |
. . 3
⊢
(∃!𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ∃*𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
| 14 | 12, 13 | syl 17 |
. 2
⊢ (𝐴 ∈ V → ∃*𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
| 15 | | eqvisset 3500 |
. . . . . . . 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 968 |
. . . . 5
⊢ (¬
𝐴 ∈ V → (((𝜑 ∧ 𝑥 = 𝐴) ∨ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) → ((𝜑 ∧ 𝑥 = 𝑦) ∨ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))))) |
| 20 | | 3orass 1090 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((𝜑 ∧ 𝑥 = 𝐴) ∨ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
| 21 | | 3orass 1090 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) ↔ ((𝜑 ∧ 𝑥 = 𝑦) ∨ ((¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
| 22 | 19, 20, 21 | 3imtr4g 296 |
. . . 4
⊢ (¬
𝐴 ∈ V → (((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
| 23 | 22 | alrimiv 1927 |
. . 3
⊢ (¬
𝐴 ∈ V →
∀𝑥(((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
| 24 | | euimmo 2616 |
. . 3
⊢
(∀𝑥(((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) → (∃!𝑥((𝜑 ∧ 𝑥 = 𝑦) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) → ∃*𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)))) |
| 25 | 23, 11, 24 | mpisyl 21 |
. 2
⊢ (¬
𝐴 ∈ V →
∃*𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶))) |
| 26 | 14, 25 | pm2.61i 182 |
1
⊢
∃*𝑥((𝜑 ∧ 𝑥 = 𝐴) ∨ (¬ (𝜑 ∨ 𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓 ∧ 𝑥 = 𝐶)) |