Proof of Theorem rmounid
Step | Hyp | Ref
| Expression |
1 | | rmounid.1 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ¬ 𝜓) |
2 | 1 | ex 413 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝐵 → ¬ 𝜓)) |
3 | 2 | con2d 134 |
. . . . . . . . . 10
⊢ (𝜑 → (𝜓 → ¬ 𝑥 ∈ 𝐵)) |
4 | 3 | imp 407 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑥 ∈ 𝐵) |
5 | | biorf 934 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))) |
6 | | orcom 867 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴)) |
7 | 5, 6 | bitr4di 289 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))) |
8 | 4, 7 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))) |
9 | | elun 4088 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) |
10 | 8, 9 | bitr4di 289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∪ 𝐵))) |
11 | 10 | pm5.32da 579 |
. . . . . 6
⊢ (𝜑 → ((𝜓 ∧ 𝑥 ∈ 𝐴) ↔ (𝜓 ∧ 𝑥 ∈ (𝐴 ∪ 𝐵)))) |
12 | 11 | biancomd 464 |
. . . . 5
⊢ (𝜑 → ((𝜓 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜓))) |
13 | 12 | bicomd 222 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜓) ↔ (𝜓 ∧ 𝑥 ∈ 𝐴))) |
14 | 13 | biancomd 464 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))) |
15 | 14 | mobidv 2551 |
. 2
⊢ (𝜑 → (∃*𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜓) ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))) |
16 | | df-rmo 3074 |
. 2
⊢
(∃*𝑥 ∈
(𝐴 ∪ 𝐵)𝜓 ↔ ∃*𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜓)) |
17 | | df-rmo 3074 |
. 2
⊢
(∃*𝑥 ∈
𝐴 𝜓 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) |
18 | 15, 16, 17 | 3bitr4g 314 |
1
⊢ (𝜑 → (∃*𝑥 ∈ (𝐴 ∪ 𝐵)𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜓)) |