Definition df-rmo 3072

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 1542	. . . . 5 class 𝑥
6	5, 3	wcel 2112	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2539	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  rmoanid  3259  nfrmo1  3298  nfrmod  3300  nfrmow  3302  nfrmo  3304  rmobida  3319  rmobiia  3322  rmoeq1f  3327  rmoeq1  3337  mormo  3351  reu5  3352  rmo5  3356  cbvrmow  3367  cbvrmovw  3375  rmov  3450  rmo4  3661  rmo3f  3665  rmoeq  3669  rmoan  3670  rmoim  3671  rmoimi2  3674  2reuswap  3677  2reu5lem2  3687  2rmoswap  3692  rmo2  3817  rmo3  3819  rmob  3820  rmob2  3822  rmoanim  3824  ssrmof  3983  dfdisj2  5037  rmorabex  5368  dffun9  6444  fncnv  6488  iunmapdisj  9685  brdom4  10192  enqeq  10596  2ndcdisj  22490  2ndcdisj2  22491  pjhtheu  29632  pjpreeq  29636  cnlnadjeui  30315  reuxfrdf  30715  rmoxfrd  30717  rmoun  30718  rmounid  30719  cbvdisjf  30786  funcnvmpt  30881  nrmo  34501  alrmomorn  36396  alrmomodm  36397  dfeldisj4  36737  cdleme0moN  38145  rmotru  46011