Definition df-rmo 2494

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 2489	. 2 wff E* x e. A ph
5	2	cv 1372	. . . . 5 class x
6	5, 3	wcel 2178	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wmo 2056	. 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  2681  cbvrmow  2691  rmobida  2696  rmobiia  2699  rmoeq1f  2704  mormo  2725  reu5  2726  rmo5  2729  rmov  2797  rmo4  2973  rmo3f  2977  rmoan  2980  rmoim  2981  rmoimi2  2983  2reuswapdc  2984  2rmorex  2986  rmo2ilem  3096  rmo3  3098  rmob  3099  ssrmof  3264  dfdisj2  4037  dffun9  5319  fncnv  5359