Definition df-rmo 2622

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 2617	. 2 wff E*x e. A ph
5	2	cv 1641	. . . . 5 class x
6	5, 3	wcel 1710	. . . 4 wff x e. A
7	6, 1	wa 358	. . 3 wff (x e. A /\ ph)
8	7, 2	wmo 2205	. 2 wff E*x(x e. A /\ ph)
9	4, 8	wb 176	1 wff (E*x e. A ph <-> E*x(x e. A /\ ph))

This definition is referenced by:  nfrmo1  2782  nfrmod  2784  nfrmo  2786  rmobida  2798  rmobiia  2801  rmoeq1f  2806  mormo  2823  reu5  2824  rmo5  2827  rmov  2875  rmo4  3029  rmoan  3034  rmoim  3035  rmoimi2  3037  2reuswap  3038  2reu5lem2  3042  rmo2  3131  rmo3  3133  rmob  3134  fncnv  5158