Step |
Hyp |
Ref |
Expression |
1 |
|
mooran2 |
⊢ ( ∃* 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) → ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ) |
2 |
|
df-rmo |
⊢ ( ∃* 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) ) |
3 |
|
elun |
⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ) |
4 |
3
|
anbi1i |
⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ 𝜑 ) ) |
5 |
|
andir |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ) |
6 |
4 5
|
bitri |
⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ) |
7 |
6
|
mobii |
⊢ ( ∃* 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) ↔ ∃* 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ) |
8 |
2 7
|
bitri |
⊢ ( ∃* 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 ↔ ∃* 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ) |
9 |
|
df-rmo |
⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) |
10 |
|
df-rmo |
⊢ ( ∃* 𝑥 ∈ 𝐵 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) |
11 |
9 10
|
anbi12i |
⊢ ( ( ∃* 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐵 𝜑 ) ↔ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ) |
12 |
1 8 11
|
3imtr4i |
⊢ ( ∃* 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 → ( ∃* 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐵 𝜑 ) ) |