Definition df-rmo 3350

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 3052). (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 3349	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2113	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2537	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3352  mormo  3355  rmobiia  3356  rmobidva  3363  rmo5  3368  cbvrmovw  3371  rmobida  3373  cbvrmow  3375  nfrmo1  3377  nfrmow  3379  rmoeq1  3381  rmoeq1OLD  3383  rmoeq1f  3389  nfrmod  3395  nfrmo  3397  rmov  3470  rmo4  3688  rmo3f  3692  rmoeq  3696  rmoan  3697  rmoim  3698  rmoimi2  3701  2reuswap  3704  2reu5lem2  3714  2rmoswap  3719  rmo2  3837  rmo3  3839  rmob  3840  rmob2  3842  rmoanim  3844  ssrmof  4001  dfdisj2  5067  rmorabex  5408  dffun9  6521  fncnv  6565  iunmapdisj  9933  brdom4  10440  enqeq  10845  2ndcdisj  23400  2ndcdisj2  23401  pjhtheu  31469  pjpreeq  31473  cnlnadjeui  32152  reuxfrdf  32565  rmoxfrd  32567  rmoun  32568  rmounid  32569  cbvdisjf  32646  funcnvmpt  32745  rmoeqi  36381  rmoeqbii  36382  rmoeqbidv  36407  disjeq12dv  36409  cbvrmovw2  36422  cbvrmodavw  36446  cbvrmodavw2  36477  nrmo  36604  alrmomorn  38551  alrmomodm  38552  dfeldisj4  38979  disjres  39003  cdleme0moN  40485  onsucf1olem  43512  tfsconcatlem  43578  modelaxreplem2  45220  rmotru  49048