Definition df-rmo 2308

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 2303	. 2 wff E*x e. A ph
5	2	cv 1241	. . . . 5 class x
6	5, 3	wcel 1390	. . . 4 wff x e. A
7	6, 1	wa 97	. . 3 wff (x e. A /\ ph)
8	7, 2	wmo 1898	. 2 wff E*x(x e. A /\ ph)
9	4, 8	wb 98	1 wff (E*x e. A ph <-> E*x(x e. A /\ ph))

This definition is referenced by:  nfrmo1  2476  rmobida  2490  rmobiia  2493  rmoeq1f  2498  mormo  2515  reu5  2516  rmo5  2519  rmov  2568  rmo4  2728  rmoan  2733  rmoim  2734  rmoimi2  2736  2reuswapdc  2737  2rmorex  2739  rmo2ilem  2841  rmo3  2843  rmob  2844  dfdisj2  3738  dffun9  4873  fncnv  4908