Definition df-rmo 2378

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 2373	. 2 wff E* x e. A ph
5	2	cv 1295	. . . . 5 class x
6	5, 3	wcel 1445	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	wmo 1956	. 2 wff E* x ( x e. A /\ ph )
9	4, 8	wb 104	1 wff ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )

This definition is referenced by:  nfrmo1  2553  rmobida  2567  rmobiia  2570  rmoeq1f  2575  mormo  2592  reu5  2593  rmo5  2596  rmov  2653  rmo4  2822  rmo3f  2826  rmoan  2829  rmoim  2830  rmoimi2  2832  2reuswapdc  2833  2rmorex  2835  rmo2ilem  2942  rmo3  2944  rmob  2945  dfdisj2  3846  dffun9  5078  fncnv  5114