Definition df-rmo 2361

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 2356	. 2 wff E* x e. A ph
5	2	cv 1284	. . . . 5 class x
6	5, 3	wcel 1434	. . . 4 wff x e. A
7	6, 1	wa 102	. . 3 wff ( x e. A /\ ph )
8	7, 2	wmo 1944	. 2 wff E* x ( x e. A /\ ph )
9	4, 8	wb 103	1 wff ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )

This definition is referenced by:  nfrmo1  2531  rmobida  2545  rmobiia  2548  rmoeq1f  2553  mormo  2570  reu5  2571  rmo5  2574  rmov  2628  rmo4  2795  rmoan  2800  rmoim  2801  rmoimi2  2803  2reuswapdc  2804  2rmorex  2806  rmo2ilem  2913  rmo3  2915  rmob  2916  dfdisj2  3789  dffun9  4981  fncnv  5017