Definition df-rmo 2314

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 2309	. 2 wff E* x e. A ph
5	2	cv 1242	. . . . 5 class x
6	5, 3	wcel 1393	. . . 4 wff x e. A
7	6, 1	wa 97	. . 3 wff ( x e. A /\ ph )
8	7, 2	wmo 1901	. 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  2482  rmobida  2496  rmobiia  2499  rmoeq1f  2504  mormo  2521  reu5  2522  rmo5  2525  rmov  2574  rmo4  2734  rmoan  2739  rmoim  2740  rmoimi2  2742  2reuswapdc  2743  2rmorex  2745  rmo2ilem  2847  rmo3  2849  rmob  2850  dfdisj2  3747  dffun9  4930  fncnv  4965