Definition df-rmo 3340

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 3050). (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 3339	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2536	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3342  mormo  3345  rmobiia  3346  rmobidva  3353  rmo5  3358  cbvrmovw  3361  rmobida  3363  cbvrmow  3365  nfrmo1  3367  nfrmow  3369  rmoeq1  3371  rmoeq1f  3377  nfrmod  3383  nfrmo  3385  rmov  3457  rmo4  3673  rmo3f  3677  rmoeq  3681  rmoan  3682  rmoim  3683  rmoimi2  3686  2reuswap  3689  2reu5lem2  3699  2rmoswap  3704  rmo2  3821  rmo3  3823  rmob  3824  rmob2  3826  rmoanim  3828  ssrmof  3984  dfdisj2  5043  rmorabex  5401  dffun9  6516  fncnv  6560  funcnvmpt  6938  iunmapdisj  9934  brdom4  10441  enqeq  10846  2ndcdisj  23409  2ndcdisj2  23410  pjhtheu  31453  pjpreeq  31457  cnlnadjeui  32136  reuxfrdf  32548  rmoxfrd  32550  rmoun  32551  rmounid  32552  cbvdisjf  32629  rmoeqi  36357  rmoeqbii  36358  rmoeqbidv  36383  disjeq12dv  36385  cbvrmovw2  36398  cbvrmodavw  36422  cbvrmodavw2  36453  nrmo  36580  alrmomorn  38667  alrmomodm  38668  dfeldisj4  39121  disjres  39153  cdleme0moN  40659  onsucf1olem  43686  tfsconcatlem  43752  modelaxreplem2  45394  rmotru  49266