Definition df-rmo 3367

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 3078). (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 3366	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1567	. . . . 5 class 𝑥
6	5, 3	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2563	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3369  mormo  3372  rmobiia  3373  rmobidva  3380  rmo5  3385  cbvrmovw  3388  rmobida  3390  cbvrmow  3392  nfrmo1  3394  nfrmow  3396  rmoeq1  3398  rmoeq1f  3404  nfrmod  3410  nfrmo  3412  rmov  3482  rmo4  3692  rmo3f  3696  rmoeq  3700  rmoan  3701  rmoim  3702  rmoimi2  3705  2reuswap  3708  2reu5lem2  3718  2rmoswap  3723  rmo2  3839  rmo3  3841  rmob  3842  rmob2  3845  rmoanim  3847  ssrmof  4004  dfdisj2  5077  rmorabex  5441  dffun9  6565  fncnv  6609  funcnvmpt  6991  iunmapdisj  10006  brdom4  10513  enqeq  10918  2ndcdisj  23592  2ndcdisj2  23593  pjhtheu  31712  pjpreeq  31716  cnlnadjeui  32395  reuxfrdf  32803  rmoxfrd  32805  rmoun  32806  rmounid  32807  cbvdisjf  32882  rmoeqi  36643  rmoeqbii  36644  rmoeqbidv  36669  disjeq12dv  36671  cbvrmovw2  36684  cbvrmodavw  36708  cbvrmodavw2  36739  nrmo  36865  alrmomorn  38953  alrmomodm  38954  dfeldisj4  39407  disjres  39439  cdleme0moN  40945  onsucf1olem  43945  tfsconcatlem  44011  modelaxreplem2  45636  rmotru  49526