Definition df-rmo 3368

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 3079). (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 3367	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1568	. . . . 5 class 𝑥
6	5, 3	wcel 2142	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2564	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  reu5  3370  mormo  3373  rmobiia  3374  rmobidva  3381  rmo5  3386  cbvrmovw  3389  rmobida  3391  cbvrmow  3393  nfrmo1  3395  nfrmow  3397  rmoeq1  3399  rmoeq1f  3405  nfrmod  3411  nfrmo  3413  rmov  3483  rmo4  3692  rmo3f  3696  rmoeq  3700  rmoan  3701  rmoim  3702  rmoimi2  3705  2reuswap  3708  2reu5lem2  3718  2rmoswap  3723  rmo2  3839  rmo3  3841  rmob  3842  rmob2  3845  rmoanim  3847  ssrmof  4004  dfdisj2  5077  rmorabex  5440  dffun9  6565  fncnv  6609  funcnvmpt  6991  iunmapdisj  10014  brdom4  10520  enqeq  10925  2ndcdisj  23624  2ndcdisj2  23625  pjhtheu  31757  pjpreeq  31761  cnlnadjeui  32440  reuxfrdf  32848  rmoxfrd  32850  rmoun  32851  rmounid  32852  cbvdisjf  32927  rmoeqi  36727  rmoeqbii  36728  rmoeqbidv  36753  disjeq12dv  36755  cbvrmovw2  36768  cbvrmodavw  36792  cbvrmodavw2  36823  nrmo  36949  alrmomorn  39035  alrmomodm  39036  dfeldisj4  39489  disjres  39521  cdleme0moN  41027  onsucf1olem  44025  tfsconcatlem  44091  modelaxreplem2  45716  rmotru  49609