Theorem rmoanim

Description: Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim . (Contributed by Alexander van der Vekens, 25-Jun-2017) Avoid ax-10 and ax-11 . (Revised by GG, 24-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		rmoanim.1	|- F/ x ph
2		impexp	|- ( ( ( ph /\ ps ) -> x = y ) <-> ( ph -> ( ps -> x = y ) ) )
3	2	ralbii	|- ( A. x e. A ( ( ph /\ ps ) -> x = y ) <-> A. x e. A ( ph -> ( ps -> x = y ) ) )
4	1	r19.21	|- ( A. x e. A ( ph -> ( ps -> x = y ) ) <-> ( ph -> A. x e. A ( ps -> x = y ) ) )
5	3 4	bitri	|- ( A. x e. A ( ( ph /\ ps ) -> x = y ) <-> ( ph -> A. x e. A ( ps -> x = y ) ) )
6	5	exbii	|- ( E. y A. x e. A ( ( ph /\ ps ) -> x = y ) <-> E. y ( ph -> A. x e. A ( ps -> x = y ) ) )
7		df-rmo	|- ( E* x e. A ( ph /\ ps ) <-> E* x ( x e. A /\ ( ph /\ ps ) ) )
8		df-mo	|- ( E* x ( x e. A /\ ( ph /\ ps ) ) <-> E. y A. x ( ( x e. A /\ ( ph /\ ps ) ) -> x = y ) )
9		impexp	|- ( ( ( x e. A /\ ( ph /\ ps ) ) -> x = y ) <-> ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) )
10	9	albii	|- ( A. x ( ( x e. A /\ ( ph /\ ps ) ) -> x = y ) <-> A. x ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) )
11		df-ral	|- ( A. x e. A ( ( ph /\ ps ) -> x = y ) <-> A. x ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) )
12	10 11	bitr4i	|- ( A. x ( ( x e. A /\ ( ph /\ ps ) ) -> x = y ) <-> A. x e. A ( ( ph /\ ps ) -> x = y ) )
13	12	exbii	|- ( E. y A. x ( ( x e. A /\ ( ph /\ ps ) ) -> x = y ) <-> E. y A. x e. A ( ( ph /\ ps ) -> x = y ) )
14	7 8 13	3bitri	|- ( E* x e. A ( ph /\ ps ) <-> E. y A. x e. A ( ( ph /\ ps ) -> x = y ) )
15		df-rmo	|- ( E* x e. A ps <-> E* x ( x e. A /\ ps ) )
16		df-mo	|- ( E* x ( x e. A /\ ps ) <-> E. y A. x ( ( x e. A /\ ps ) -> x = y ) )
17		impexp	|- ( ( ( x e. A /\ ps ) -> x = y ) <-> ( x e. A -> ( ps -> x = y ) ) )
18	17	albii	|- ( A. x ( ( x e. A /\ ps ) -> x = y ) <-> A. x ( x e. A -> ( ps -> x = y ) ) )
19		df-ral	|- ( A. x e. A ( ps -> x = y ) <-> A. x ( x e. A -> ( ps -> x = y ) ) )
20	18 19	bitr4i	|- ( A. x ( ( x e. A /\ ps ) -> x = y ) <-> A. x e. A ( ps -> x = y ) )
21	20	exbii	|- ( E. y A. x ( ( x e. A /\ ps ) -> x = y ) <-> E. y A. x e. A ( ps -> x = y ) )
22	15 16 21	3bitri	|- ( E* x e. A ps <-> E. y A. x e. A ( ps -> x = y ) )
23	22	imbi2i	|- ( ( ph -> E* x e. A ps ) <-> ( ph -> E. y A. x e. A ( ps -> x = y ) ) )
24		19.37v	|- ( E. y ( ph -> A. x e. A ( ps -> x = y ) ) <-> ( ph -> E. y A. x e. A ( ps -> x = y ) ) )
25	23 24	bitr4i	|- ( ( ph -> E* x e. A ps ) <-> E. y ( ph -> A. x e. A ( ps -> x = y ) ) )
26	6 14 25	3bitr4i	|- ( E* x e. A ( ph /\ ps ) <-> ( ph -> E* x e. A ps ) )