Definition df-rmo 2492

Description: Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)

Assertion

Ref	Expression
df-rmo	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )

Detailed syntax breakdown of Definition df-rmo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	wrmo 2487	. 2 wff E* x e. A ph
5	2	cv 1372	. . . . 5 class x
6	5, 3	wcel 2176	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wmo 2055	. 2 wff E* x ( x e. A /\ ph )
9	4, 8	wb 105	1 wff ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )

This definition is referenced by:  nfrmo1  2679  rmobida  2693  rmobiia  2696  rmoeq1f  2701  mormo  2722  reu5  2723  rmo5  2726  rmov  2792  rmo4  2966  rmo3f  2970  rmoan  2973  rmoim  2974  rmoimi2  2976  2reuswapdc  2977  2rmorex  2979  rmo2ilem  3088  rmo3  3090  rmob  3091  ssrmof  3256  dfdisj2  4023  dffun9  5300  fncnv  5340