Definition df-rmo 3388

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 3068). (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 3387	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1536	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2541	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3390  mormo  3393  rmobiia  3394  rmoanidOLD  3400  rmobidva  3403  rmo5  3408  cbvrmovw  3411  rmobida  3414  cbvrmow  3417  nfrmo1  3419  nfrmow  3421  rmoeq1  3425  rmoeq1OLD  3427  rmoeq1f  3431  nfrmowOLD  3434  nfrmod  3439  nfrmo  3441  rmov  3519  rmo4  3752  rmo3f  3756  rmoeq  3760  rmoan  3761  rmoim  3762  rmoimi2  3765  2reuswap  3768  2reu5lem2  3778  2rmoswap  3783  rmo2  3909  rmo3  3911  rmob  3912  rmob2  3914  rmoanim  3916  ssrmof  4076  dfdisj2  5135  rmorabex  5480  dffun9  6607  fncnv  6651  iunmapdisj  10092  brdom4  10599  enqeq  11003  2ndcdisj  23485  2ndcdisj2  23486  pjhtheu  31426  pjpreeq  31430  cnlnadjeui  32109  reuxfrdf  32519  rmoxfrd  32521  rmoun  32522  rmounid  32523  cbvdisjf  32593  funcnvmpt  32685  rmoeqi  36151  rmoeqbii  36152  rmoeqbidv  36177  disjeq12dv  36181  cbvrmovw2  36194  cbvrmodavw  36218  cbvrmodavw2  36249  nrmo  36376  alrmomorn  38314  alrmomodm  38315  dfeldisj4  38676  disjres  38700  cdleme0moN  40182  onsucf1olem  43232  tfsconcatlem  43298  rmotru  48536