Definition df-rmo 3377

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 3059). (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 3376	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1535	. . . . 5 class 𝑥
6	5, 3	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2535	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3379  mormo  3382  rmobiia  3383  rmoanidOLD  3389  rmobidva  3392  rmo5  3397  cbvrmovw  3400  rmobida  3403  cbvrmow  3406  nfrmo1  3408  nfrmow  3410  rmoeq1  3413  rmoeq1OLD  3415  rmoeq1f  3420  nfrmowOLD  3423  nfrmod  3428  nfrmo  3430  rmov  3508  rmo4  3738  rmo3f  3742  rmoeq  3746  rmoan  3747  rmoim  3748  rmoimi2  3751  2reuswap  3754  2reu5lem2  3764  2rmoswap  3769  rmo2  3895  rmo3  3897  rmob  3898  rmob2  3900  rmoanim  3902  ssrmof  4062  dfdisj2  5116  rmorabex  5470  dffun9  6596  fncnv  6640  iunmapdisj  10060  brdom4  10567  enqeq  10971  2ndcdisj  23479  2ndcdisj2  23480  pjhtheu  31422  pjpreeq  31426  cnlnadjeui  32105  reuxfrdf  32518  rmoxfrd  32520  rmoun  32521  rmounid  32522  cbvdisjf  32590  funcnvmpt  32683  rmoeqi  36168  rmoeqbii  36169  rmoeqbidv  36194  disjeq12dv  36197  cbvrmovw2  36210  cbvrmodavw  36234  cbvrmodavw2  36265  nrmo  36392  alrmomorn  38339  alrmomodm  38340  dfeldisj4  38701  disjres  38725  cdleme0moN  40207  onsucf1olem  43259  tfsconcatlem  43325  modelaxreplem2  44943  rmotru  48651