Theorem rmounid

Description: A case where an "at most one" restricted existential quantifier for a union is equivalent to such a quantifier for one of the sets. (Contributed by Thierry Arnoux, 27-Nov-2023)

	Ref	Expression
Hypothesis	rmounid.1	|- ( ( ph /\ x e. B ) -> -. ps )
Assertion	rmounid	|- ( ph -> ( E* x e. ( A u. B ) ps <-> E* x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		rmounid.1	|- ( ( ph /\ x e. B ) -> -. ps )
2	1	ex	|- ( ph -> ( x e. B -> -. ps ) )
3	2	con2d	|- ( ph -> ( ps -> -. x e. B ) )
4	3	imp	|- ( ( ph /\ ps ) -> -. x e. B )
5		biorf	|- ( -. x e. B -> ( x e. A <-> ( x e. B \/ x e. A ) ) )
6		orcom	|- ( ( x e. A \/ x e. B ) <-> ( x e. B \/ x e. A ) )
7	5 6	bitr4di	|- ( -. x e. B -> ( x e. A <-> ( x e. A \/ x e. B ) ) )
8	4 7	syl	|- ( ( ph /\ ps ) -> ( x e. A <-> ( x e. A \/ x e. B ) ) )
9		elun	|- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
10	8 9	bitr4di	|- ( ( ph /\ ps ) -> ( x e. A <-> x e. ( A u. B ) ) )
11	10	pm5.32da	|- ( ph -> ( ( ps /\ x e. A ) <-> ( ps /\ x e. ( A u. B ) ) ) )
12	11	biancomd	|- ( ph -> ( ( ps /\ x e. A ) <-> ( x e. ( A u. B ) /\ ps ) ) )
13	12	bicomd	|- ( ph -> ( ( x e. ( A u. B ) /\ ps ) <-> ( ps /\ x e. A ) ) )
14	13	biancomd	|- ( ph -> ( ( x e. ( A u. B ) /\ ps ) <-> ( x e. A /\ ps ) ) )
15	14	mobidv	|- ( ph -> ( E* x ( x e. ( A u. B ) /\ ps ) <-> E* x ( x e. A /\ ps ) ) )
16		df-rmo	|- ( E* x e. ( A u. B ) ps <-> E* x ( x e. ( A u. B ) /\ ps ) )
17		df-rmo	|- ( E* x e. A ps <-> E* x ( x e. A /\ ps ) )
18	15 16 17	3bitr4g	|- ( ph -> ( E* x e. ( A u. B ) ps <-> E* x e. A ps ) )