Definition df-rmo 2331

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 2326	. 2 wff E* x e. A ph
5	2	cv 1258	. . . . 5 class x
6	5, 3	wcel 1409	. . . 4 wff x e. A
7	6, 1	wa 101	. . 3 wff ( x e. A /\ ph )
8	7, 2	wmo 1917	. 2 wff E* x ( x e. A /\ ph )
9	4, 8	wb 102	1 wff ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )

This definition is referenced by:  nfrmo1  2499  rmobida  2513  rmobiia  2516  rmoeq1f  2521  mormo  2538  reu5  2539  rmo5  2542  rmov  2591  rmo4  2756  rmoan  2761  rmoim  2762  rmoimi2  2764  2reuswapdc  2765  2rmorex  2767  rmo2ilem  2874  rmo3  2876  rmob  2877  dfdisj2  3774  dffun9  4957  fncnv  4992