Theorem rmoun

Description: "At most one" restricted existential quantifier for a union implies the same quantifier on both sets. (Contributed by Thierry Arnoux, 27-Nov-2023)

	Ref	Expression
Assertion	rmoun	|- ( E* x e. ( A u. B ) ph -> ( E* x e. A ph /\ E* x e. B ph ) )

Proof

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 ) )