Definition df-rmo 3380

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 3062). (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 3379	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 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  3382  mormo  3385  rmobiia  3386  rmoanidOLD  3392  rmobidva  3395  rmo5  3400  cbvrmovw  3403  rmobida  3406  cbvrmow  3409  nfrmo1  3411  nfrmow  3413  rmoeq1  3416  rmoeq1OLD  3418  rmoeq1f  3424  nfrmowOLD  3427  nfrmod  3432  nfrmo  3434  rmov  3511  rmo4  3736  rmo3f  3740  rmoeq  3744  rmoan  3745  rmoim  3746  rmoimi2  3749  2reuswap  3752  2reu5lem2  3762  2rmoswap  3767  rmo2  3887  rmo3  3889  rmob  3890  rmob2  3892  rmoanim  3894  ssrmof  4051  dfdisj2  5112  rmorabex  5465  dffun9  6595  fncnv  6639  iunmapdisj  10063  brdom4  10570  enqeq  10974  2ndcdisj  23464  2ndcdisj2  23465  pjhtheu  31413  pjpreeq  31417  cnlnadjeui  32096  reuxfrdf  32510  rmoxfrd  32512  rmoun  32513  rmounid  32514  cbvdisjf  32584  funcnvmpt  32677  rmoeqi  36188  rmoeqbii  36189  rmoeqbidv  36214  disjeq12dv  36216  cbvrmovw2  36229  cbvrmodavw  36253  cbvrmodavw2  36284  nrmo  36411  alrmomorn  38359  alrmomodm  38360  dfeldisj4  38721  disjres  38745  cdleme0moN  40227  onsucf1olem  43283  tfsconcatlem  43349  modelaxreplem2  44996  rmotru  48723