Definition df-rmo 2463

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 2458	. 2 wff E* x e. A ph
5	2	cv 1352	. . . . 5 class x
6	5, 3	wcel 2148	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wmo 2027	. 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  2650  rmobida  2664  rmobiia  2667  rmoeq1f  2672  mormo  2689  reu5  2690  rmo5  2693  rmov  2759  rmo4  2932  rmo3f  2936  rmoan  2939  rmoim  2940  rmoimi2  2942  2reuswapdc  2943  2rmorex  2945  rmo2ilem  3054  rmo3  3056  rmob  3057  ssrmof  3220  dfdisj2  3984  dffun9  5247  fncnv  5284