Step |
Hyp |
Ref |
Expression |
1 |
|
mooran2 |
|- ( E* x ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) -> ( E* x ( x e. A /\ ph ) /\ E* x ( x e. B /\ ph ) ) ) |
2 |
|
df-rmo |
|- ( E* x e. ( A u. B ) ph <-> E* x ( x e. ( A u. B ) /\ ph ) ) |
3 |
|
elun |
|- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) ) |
4 |
3
|
anbi1i |
|- ( ( x e. ( A u. B ) /\ ph ) <-> ( ( x e. A \/ x e. B ) /\ ph ) ) |
5 |
|
andir |
|- ( ( ( x e. A \/ x e. B ) /\ ph ) <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) ) |
6 |
4 5
|
bitri |
|- ( ( x e. ( A u. B ) /\ ph ) <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) ) |
7 |
6
|
mobii |
|- ( E* x ( x e. ( A u. B ) /\ ph ) <-> E* x ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) ) |
8 |
2 7
|
bitri |
|- ( E* x e. ( A u. B ) ph <-> E* x ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) ) |
9 |
|
df-rmo |
|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) ) |
10 |
|
df-rmo |
|- ( E* x e. B ph <-> E* x ( x e. B /\ ph ) ) |
11 |
9 10
|
anbi12i |
|- ( ( E* x e. A ph /\ E* x e. B ph ) <-> ( E* x ( x e. A /\ ph ) /\ E* x ( x e. B /\ ph ) ) ) |
12 |
1 8 11
|
3imtr4i |
|- ( E* x e. ( A u. B ) ph -> ( E* x e. A ph /\ E* x e. B ph ) ) |