Definition df-rmo 3071

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 3069). (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 3067	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1538	. . . . 5 class 𝑥
6	5, 3	wcel 2106	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 396	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2538	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  rmoanid  3299  nfrmo1  3301  nfrmod  3303  nfrmow  3304  nfrmowOLD  3307  nfrmo  3309  rmobida  3326  rmobidva  3327  rmobiia  3330  rmoeq1f  3335  rmoeq1  3345  mormo  3360  reu5  3361  rmo5  3365  cbvrmow  3375  cbvrmovw  3385  rmov  3459  rmo4  3665  rmo3f  3669  rmoeq  3673  rmoan  3674  rmoim  3675  rmoimi2  3678  2reuswap  3681  2reu5lem2  3691  2rmoswap  3696  rmo2  3820  rmo3  3822  rmob  3823  rmob2  3825  rmoanim  3827  ssrmof  3986  dfdisj2  5041  rmorabex  5375  dffun9  6463  fncnv  6507  iunmapdisj  9779  brdom4  10286  enqeq  10690  2ndcdisj  22607  2ndcdisj2  22608  pjhtheu  29756  pjpreeq  29760  cnlnadjeui  30439  reuxfrdf  30839  rmoxfrd  30841  rmoun  30842  rmounid  30843  cbvdisjf  30910  funcnvmpt  31004  nrmo  34599  alrmomorn  36490  alrmomodm  36491  dfeldisj4  36831  cdleme0moN  38239  rmotru  46150