Definition df-rmo 2483

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 2478	. 2 wff E* x e. A ph
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2167	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wmo 2046	. 2 wff E* x ( x e. A /\ ph )
9	4, 8	wb 105	1 wff ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )

This definition is referenced by:  nfrmo1  2670  rmobida  2684  rmobiia  2687  rmoeq1f  2692  mormo  2713  reu5  2714  rmo5  2717  rmov  2783  rmo4  2957  rmo3f  2961  rmoan  2964  rmoim  2965  rmoimi2  2967  2reuswapdc  2968  2rmorex  2970  rmo2ilem  3079  rmo3  3081  rmob  3082  ssrmof  3246  dfdisj2  4012  dffun9  5287  fncnv  5324