Definition df-rmo 3146

Description: Define restricted "at most one".

Note: This notation is most often used to express that 𝜑 holds for at most one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint.

Should instead 𝐴 depend on 𝑥, you rather assert at most one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3143). (Contributed by NM, 16-Jun-2017.)

Assertion

Ref	Expression
df-rmo	⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

Detailed syntax breakdown of Definition df-rmo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wrmo 3141	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1536	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 398	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2620	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 208	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  rmoanid  3329  nfrmo1  3371  nfrmod  3373  nfrmow  3375  nfrmo  3377  rmobida  3392  rmobiia  3395  rmoeq1f  3400  rmoeq1  3408  mormo  3429  reu5  3430  rmo5  3434  rmov  3522  rmo4  3721  rmo3f  3725  rmoeq  3729  rmoan  3730  rmoim  3731  rmoimi2  3734  2reuswap  3737  2reu5lem2  3747  2rmoswap  3752  rmo2  3870  rmo3  3872  rmo3OLD  3873  rmob  3874  rmob2  3876  rmoanim  3878  ssrmof  4032  dfdisj2  5033  rmorabex  5352  dffun9  6384  fncnv  6427  iunmapdisj  9449  brdom4  9952  enqeq  10356  2ndcdisj  22064  2ndcdisj2  22065  pjhtheu  29171  pjpreeq  29175  cnlnadjeui  29854  reuxfrdf  30255  rmoxfrd  30257  rmoun  30258  rmounid  30259  cbvdisjf  30321  funcnvmpt  30412  nrmo  33758  alrmomorn  35627  alrmomodm  35628  dfeldisj4  35968  cdleme0moN  37376