Definition df-rmo 3351

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 3350	. 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  3353  mormo  3356  rmobiia  3357  rmobidva  3364  rmo5  3369  cbvrmovw  3372  rmobida  3374  cbvrmow  3376  nfrmo1  3378  nfrmow  3380  rmoeq1  3382  rmoeq1OLD  3384  rmoeq1f  3390  nfrmod  3396  nfrmo  3398  rmov  3471  rmo4  3689  rmo3f  3693  rmoeq  3697  rmoan  3698  rmoim  3699  rmoimi2  3702  2reuswap  3705  2reu5lem2  3715  2rmoswap  3720  rmo2  3838  rmo3  3840  rmob  3841  rmob2  3843  rmoanim  3845  ssrmof  4002  dfdisj2  5068  rmorabex  5409  dffun9  6522  fncnv  6566  funcnvmpt  6944  iunmapdisj  9937  brdom4  10444  enqeq  10849  2ndcdisj  23404  2ndcdisj2  23405  pjhtheu  31473  pjpreeq  31477  cnlnadjeui  32156  reuxfrdf  32568  rmoxfrd  32570  rmoun  32571  rmounid  32572  cbvdisjf  32649  rmoeqi  36383  rmoeqbii  36384  rmoeqbidv  36409  disjeq12dv  36411  cbvrmovw2  36424  cbvrmodavw  36448  cbvrmodavw2  36479  nrmo  36606  alrmomorn  38561  alrmomodm  38562  dfeldisj4  39015  disjres  39047  cdleme0moN  40553  onsucf1olem  43579  tfsconcatlem  43645  modelaxreplem2  45287  rmotru  49115