Definition df-rmo 2528

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 2523	. 2 wff E* x e. A ph
5	2	cv 1397	. . . . 5 class x
6	5, 3	wcel 2203	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wmo 2081	. 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  2716  cbvrmow  2726  rmobida  2731  rmobiia  2734  rmoeq1f  2739  mormo  2760  reu5  2761  rmo5  2764  rmov  2833  rmo4  3009  rmo3f  3013  rmoan  3016  rmoim  3017  rmoimi2  3019  2reuswapdc  3020  2rmorex  3022  rmo2ilem  3132  rmo3  3134  rmob  3135  ssrmof  3300  dfdisj2  4086  dffun9  5380  fncnv  5421