Definition df-rmo 3078

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

This definition is referenced by:  rmoanid  3252  nfrmo1  3289  nfrmod  3291  nfrmow  3293  nfrmo  3295  rmobida  3310  rmobiia  3313  rmoeq1f  3318  rmoeq1  3326  mormo  3339  reu5  3340  rmo5  3344  cbvrmow  3355  rmov  3438  rmo4  3644  rmo3f  3648  rmoeq  3652  rmoan  3653  rmoim  3654  rmoimi2  3657  2reuswap  3660  2reu5lem2  3670  2rmoswap  3675  rmo2  3793  rmo3  3795  rmob  3796  rmob2  3798  rmoanim  3800  ssrmof  3957  dfdisj2  4999  rmorabex  5320  dffun9  6364  fncnv  6408  iunmapdisj  9483  brdom4  9990  enqeq  10394  2ndcdisj  22156  2ndcdisj2  22157  pjhtheu  29276  pjpreeq  29280  cnlnadjeui  29959  reuxfrdf  30361  rmoxfrd  30363  rmoun  30364  rmounid  30365  cbvdisjf  30432  funcnvmpt  30528  nrmo  34148  alrmomorn  36052  alrmomodm  36053  dfeldisj4  36393  cdleme0moN  37801