Definition df-rmo 3352

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 3351	. 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  3354  mormo  3357  rmobiia  3358  rmobidva  3365  rmo5  3370  cbvrmovw  3373  rmobida  3375  cbvrmow  3377  nfrmo1  3379  nfrmow  3381  rmoeq1  3383  rmoeq1OLD  3385  rmoeq1f  3391  nfrmod  3397  nfrmo  3399  rmov  3472  rmo4  3690  rmo3f  3694  rmoeq  3698  rmoan  3699  rmoim  3700  rmoimi2  3703  2reuswap  3706  2reu5lem2  3716  2rmoswap  3721  rmo2  3839  rmo3  3841  rmob  3842  rmob2  3844  rmoanim  3846  ssrmof  4003  dfdisj2  5069  rmorabex  5417  dffun9  6531  fncnv  6575  funcnvmpt  6953  iunmapdisj  9947  brdom4  10454  enqeq  10859  2ndcdisj  23417  2ndcdisj2  23418  pjhtheu  31488  pjpreeq  31492  cnlnadjeui  32171  reuxfrdf  32583  rmoxfrd  32585  rmoun  32586  rmounid  32587  cbvdisjf  32664  rmoeqi  36409  rmoeqbii  36410  rmoeqbidv  36435  disjeq12dv  36437  cbvrmovw2  36450  cbvrmodavw  36474  cbvrmodavw2  36505  nrmo  36632  alrmomorn  38638  alrmomodm  38639  dfeldisj4  39092  disjres  39124  cdleme0moN  40630  onsucf1olem  43656  tfsconcatlem  43722  modelaxreplem2  45364  rmotru  49191