Definition df-rmo 3369

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 3368	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1561	. . . . 5 class 𝑥
6	5, 3	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2566	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 208	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3371  mormo  3374  rmobiia  3375  rmobidva  3382  rmo5  3387  cbvrmovw  3390  rmobida  3392  cbvrmow  3394  nfrmo1  3396  nfrmow  3398  rmoeq1  3400  rmoeq1f  3406  nfrmod  3412  nfrmo  3414  rmov  3485  rmo4  3695  rmo3f  3699  rmoeq  3703  rmoan  3704  rmoim  3705  rmoimi2  3708  2reuswap  3711  2reu5lem2  3721  2rmoswap  3726  rmo2  3842  rmo3  3844  rmob  3845  rmob2  3847  rmoanim  3849  ssrmof  4006  dfdisj2  5071  rmorabex  5429  dffun9  6552  fncnv  6596  funcnvmpt  6979  iunmapdisj  9981  brdom4  10489  enqeq  10894  2ndcdisj  23518  2ndcdisj2  23519  pjhtheu  31599  pjpreeq  31603  cnlnadjeui  32282  reuxfrdf  32692  rmoxfrd  32694  rmoun  32695  rmounid  32696  cbvdisjf  32773  rmoeqi  36552  rmoeqbii  36553  rmoeqbidv  36578  disjeq12dv  36580  cbvrmovw2  36593  cbvrmodavw  36617  cbvrmodavw2  36648  nrmo  36775  alrmomorn  38862  alrmomodm  38863  dfeldisj4  39316  disjres  39348  cdleme0moN  40854  onsucf1olem  43852  tfsconcatlem  43918  modelaxreplem2  45560  rmotru  49429