Definition df-rmo 3346

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 3048). (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 3345	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2111	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2533	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3348  mormo  3351  rmobiia  3352  rmobidva  3359  rmo5  3364  cbvrmovw  3367  rmobida  3369  cbvrmow  3371  nfrmo1  3373  nfrmow  3375  rmoeq1  3377  rmoeq1OLD  3379  rmoeq1f  3385  nfrmod  3391  nfrmo  3393  rmov  3466  rmo4  3684  rmo3f  3688  rmoeq  3692  rmoan  3693  rmoim  3694  rmoimi2  3697  2reuswap  3700  2reu5lem2  3710  2rmoswap  3715  rmo2  3833  rmo3  3835  rmob  3836  rmob2  3838  rmoanim  3840  ssrmof  3997  dfdisj2  5058  rmorabex  5398  dffun9  6510  fncnv  6554  iunmapdisj  9914  brdom4  10421  enqeq  10825  2ndcdisj  23371  2ndcdisj2  23372  pjhtheu  31374  pjpreeq  31378  cnlnadjeui  32057  reuxfrdf  32470  rmoxfrd  32472  rmoun  32473  rmounid  32474  cbvdisjf  32551  funcnvmpt  32649  rmoeqi  36231  rmoeqbii  36232  rmoeqbidv  36257  disjeq12dv  36259  cbvrmovw2  36272  cbvrmodavw  36296  cbvrmodavw2  36327  nrmo  36454  alrmomorn  38400  alrmomodm  38401  dfeldisj4  38828  disjres  38852  cdleme0moN  40334  onsucf1olem  43373  tfsconcatlem  43439  modelaxreplem2  45082  rmotru  48913