Definition df-rmo 3354

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 3045). (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 3353	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2109	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2531	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3356  mormo  3359  rmobiia  3360  rmoanidOLD  3366  rmobidva  3369  rmo5  3374  cbvrmovw  3377  rmobida  3379  cbvrmow  3381  nfrmo1  3383  nfrmow  3385  rmoeq1  3387  rmoeq1OLD  3389  rmoeq1f  3395  nfrmod  3401  nfrmo  3403  rmov  3477  rmo4  3701  rmo3f  3705  rmoeq  3709  rmoan  3710  rmoim  3711  rmoimi2  3714  2reuswap  3717  2reu5lem2  3727  2rmoswap  3732  rmo2  3850  rmo3  3852  rmob  3853  rmob2  3855  rmoanim  3857  ssrmof  4014  dfdisj2  5076  rmorabex  5420  dffun9  6545  fncnv  6589  iunmapdisj  9976  brdom4  10483  enqeq  10887  2ndcdisj  23343  2ndcdisj2  23344  pjhtheu  31323  pjpreeq  31327  cnlnadjeui  32006  reuxfrdf  32420  rmoxfrd  32422  rmoun  32423  rmounid  32424  cbvdisjf  32500  funcnvmpt  32591  rmoeqi  36175  rmoeqbii  36176  rmoeqbidv  36201  disjeq12dv  36203  cbvrmovw2  36216  cbvrmodavw  36240  cbvrmodavw2  36271  nrmo  36398  alrmomorn  38340  alrmomodm  38341  dfeldisj4  38712  disjres  38736  cdleme0moN  40219  onsucf1olem  43259  tfsconcatlem  43325  modelaxreplem2  44969  rmotru  48788