Definition df-rmo 2461

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 2456	. 2 wff E* x e. A ph
5	2	cv 1352	. . . . 5 class x
6	5, 3	wcel 2146	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wmo 2025	. 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  2647  rmobida  2661  rmobiia  2664  rmoeq1f  2669  mormo  2686  reu5  2687  rmo5  2690  rmov  2755  rmo4  2928  rmo3f  2932  rmoan  2935  rmoim  2936  rmoimi2  2938  2reuswapdc  2939  2rmorex  2941  rmo2ilem  3050  rmo3  3052  rmob  3053  ssrmof  3216  dfdisj2  3977  dffun9  5237  fncnv  5274