Definition df-rmo 3343

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 3342	. 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  3345  mormo  3348  rmobiia  3349  rmoanidOLD  3355  rmobidva  3358  rmo5  3363  cbvrmovw  3366  rmobida  3368  cbvrmow  3370  nfrmo1  3372  nfrmow  3374  rmoeq1  3376  rmoeq1OLD  3378  rmoeq1f  3384  nfrmod  3390  nfrmo  3392  rmov  3466  rmo4  3690  rmo3f  3694  rmoeq  3698  rmoan  3699  rmoim  3700  rmoimi2  3703  2reuswap  3706  2reu5lem2  3716  2rmoswap  3721  rmo2  3839  rmo3  3841  rmob  3842  rmob2  3844  rmoanim  3846  ssrmof  4003  dfdisj2  5061  rmorabex  5403  dffun9  6511  fncnv  6555  iunmapdisj  9917  brdom4  10424  enqeq  10828  2ndcdisj  23341  2ndcdisj2  23342  pjhtheu  31338  pjpreeq  31342  cnlnadjeui  32021  reuxfrdf  32435  rmoxfrd  32437  rmoun  32438  rmounid  32439  cbvdisjf  32515  funcnvmpt  32611  rmoeqi  36171  rmoeqbii  36172  rmoeqbidv  36197  disjeq12dv  36199  cbvrmovw2  36212  cbvrmodavw  36236  cbvrmodavw2  36267  nrmo  36394  alrmomorn  38336  alrmomodm  38337  dfeldisj4  38708  disjres  38732  cdleme0moN  40214  onsucf1olem  43253  tfsconcatlem  43319  modelaxreplem2  44963  rmotru  48797