Definition df-rmo 3351

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 3350	. 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  3353  mormo  3356  rmobiia  3357  rmoanidOLD  3363  rmobidva  3366  rmo5  3371  cbvrmovw  3374  rmobida  3376  cbvrmow  3378  nfrmo1  3380  nfrmow  3382  rmoeq1  3384  rmoeq1OLD  3386  rmoeq1f  3392  nfrmod  3398  nfrmo  3400  rmov  3474  rmo4  3698  rmo3f  3702  rmoeq  3706  rmoan  3707  rmoim  3708  rmoimi2  3711  2reuswap  3714  2reu5lem2  3724  2rmoswap  3729  rmo2  3847  rmo3  3849  rmob  3850  rmob2  3852  rmoanim  3854  ssrmof  4011  dfdisj2  5071  rmorabex  5415  dffun9  6529  fncnv  6573  iunmapdisj  9952  brdom4  10459  enqeq  10863  2ndcdisj  23319  2ndcdisj2  23320  pjhtheu  31296  pjpreeq  31300  cnlnadjeui  31979  reuxfrdf  32393  rmoxfrd  32395  rmoun  32396  rmounid  32397  cbvdisjf  32473  funcnvmpt  32564  rmoeqi  36148  rmoeqbii  36149  rmoeqbidv  36174  disjeq12dv  36176  cbvrmovw2  36189  cbvrmodavw  36213  cbvrmodavw2  36244  nrmo  36371  alrmomorn  38313  alrmomodm  38314  dfeldisj4  38685  disjres  38709  cdleme0moN  40192  onsucf1olem  43232  tfsconcatlem  43298  modelaxreplem2  44942  rmotru  48764