Definition df-rmo 3343

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 3053). (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 3342	. 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 2538	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3345  mormo  3348  rmobiia  3349  rmobidva  3356  rmo5  3361  cbvrmovw  3364  rmobida  3366  cbvrmow  3368  nfrmo1  3370  nfrmow  3372  rmoeq1  3374  rmoeq1f  3380  nfrmod  3386  nfrmo  3388  rmov  3460  rmo4  3677  rmo3f  3681  rmoeq  3685  rmoan  3686  rmoim  3687  rmoimi2  3690  2reuswap  3693  2reu5lem2  3703  2rmoswap  3708  rmo2  3826  rmo3  3828  rmob  3829  rmob2  3831  rmoanim  3833  ssrmof  3990  dfdisj2  5055  rmorabex  5411  dffun9  6525  fncnv  6569  funcnvmpt  6947  iunmapdisj  9942  brdom4  10449  enqeq  10854  2ndcdisj  23418  2ndcdisj2  23419  pjhtheu  31462  pjpreeq  31466  cnlnadjeui  32145  reuxfrdf  32557  rmoxfrd  32559  rmoun  32560  rmounid  32561  cbvdisjf  32638  rmoeqi  36366  rmoeqbii  36367  rmoeqbidv  36392  disjeq12dv  36394  cbvrmovw2  36407  cbvrmodavw  36431  cbvrmodavw2  36462  nrmo  36589  alrmomorn  38676  alrmomodm  38677  dfeldisj4  39130  disjres  39162  cdleme0moN  40668  onsucf1olem  43695  tfsconcatlem  43761  modelaxreplem2  45403  rmotru  49269